Skip to content

Commit fa6418a

Browse files
xroblotxroblot
committed
feat(FieldTheory/IntermediateField): define the image of an intermediate field in a larger extension (#36772)
Given a tower of fields `K ⊆ L ⊆ M` and an intermediate field `F` of `L/K`, defines `IntermediateField.extendTop F M` as the image of `F` under` L →ₐ[K] M`, together with instances transferring `Algebra`, `IsFractionRing` and `IsIntegralClosure` to the image. The main motivation is to embed a subextension `F/K` of `L/K` into a larger extension `M/K`. This is useful for instance when one needs `M/K` to be Galois. This construction will be useful in a later PR to prove that the compositum of two unramified extensions is unramified. Indeed, the result is first proved when the two extensions are `IntermediateField K L` with `L/K` Galois, and then in the general case (see #36843)
1 parent 03ab904 commit fa6418a

File tree

4 files changed

+153
-0
lines changed

4 files changed

+153
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4357,6 +4357,7 @@ public import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
43574357
public import Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
43584358
public import Mathlib.FieldTheory.IntermediateField.Algebraic
43594359
public import Mathlib.FieldTheory.IntermediateField.Basic
4360+
public import Mathlib.FieldTheory.IntermediateField.ExtendRight
43604361
public import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
43614362
public import Mathlib.FieldTheory.IsAlgClosed.Basic
43624363
public import Mathlib.FieldTheory.IsAlgClosed.Classification

‎Mathlib/Algebra/Algebra/Hom.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -107,6 +107,10 @@ instance algHomClass : AlgHomClass (A →ₐ[R] B) R A B where
107107
map_one f := f.map_one'
108108
commutes f := f.commutes'
109109

110+
lemma _root_.Algebra.algHom_apply (R A B : Type*) [CommSemiring R] [CommSemiring A] [Semiring B]
111+
[Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (x : A) :
112+
Algebra.algHom R A B x = algebraMap A B x := rfl
113+
110114
@[simp] lemma _root_.AlgHomClass.toLinearMap_toAlgHom {R A B F : Type*} [CommSemiring R]
111115
[Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [FunLike F A B] [AlgHomClass F R A B]
112116
(f : F) : (AlgHomClass.toAlgHom f : A →ₗ[R] B) = f := rfl

‎Mathlib/FieldTheory/IntermediateField/ExtendRight.lean‎

Lines changed: 143 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,143 @@
1+
/-
2+
Copyright (c) 2026 Xavier Roblot. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Xavier Roblot
5+
-/
6+
module
7+
8+
public import Mathlib.FieldTheory.IntermediateField.Basic
9+
public import Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
10+
11+
/-!
12+
# Extending intermediate fields to a larger extension
13+
14+
Given a tower of field extensions `K ⊆ L ⊆ M` and an intermediate field `F` of `L/K`, this file
15+
defines `IntermediateField.extendRight F M`, the image of `F` under the inclusion `L ⊆ M`,
16+
as an intermediate field of `M/K`. It is canonically isomorphic to `F` as a `K`-algebra.
17+
18+
The main motivation is to embed a subextension `F/K` of `L/K` into a larger extension `M/K`.
19+
This is useful for instance when one needs `M/K` to be Galois.
20+
21+
## Main definitions
22+
23+
- `IntermediateField.extendRight F M`: the intermediate field of `M/K` defined as the image of `F`
24+
under the map `L →ₐ[K] M`.
25+
- `IntermediateField.extendRightEquiv F M`: the `K`-algebra isomorphism `F ≃ₐ[K] extendRight F M`.
26+
27+
## Main instances
28+
29+
- `IntermediateField.extendRight.algebra`: for `S` with `Algebra S F`, `S` acts
30+
on `extendRight F M`.
31+
- `IntermediateField.extendRight.isFractionRing`: transfers the `IsFractionRing S F` instance.
32+
- `IntermediateField.extendRight.isIntegralClosure`: transfers the
33+
`IsIntegralClosure S R F` instance.
34+
-/
35+
36+
@[expose] public section
37+
38+
namespace IntermediateField
39+
40+
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L)
41+
(M : Type*) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M]
42+
43+
/--
44+
The image of the intermediate field `F` of `L/K` under the inclusion `L ⊆ M`, viewed as an
45+
intermediate field of `M/K`.
46+
-/
47+
def extendRight : IntermediateField K M := F.map (Algebra.algHom K L M)
48+
49+
/-- The isomorphism between `F` and its image `F.extendRight M` in `M`. -/
50+
noncomputable def extendRightEquiv : F ≃ₐ[K] (F.extendRight M) := F.equivMap (Algebra.algHom K L M)
51+
52+
@[simp]
53+
theorem algebraMap_extendRightEquiv (a : F) :
54+
algebraMap (F.extendRight M) M (extendRightEquiv F M a) = algebraMap F M a := rfl
55+
56+
@[simp]
57+
theorem coe_extendRightEquiv (a : F) :
58+
(extendRightEquiv F M a : M) = algebraMap F M a := rfl
59+
60+
@[simp]
61+
theorem algebraMap_extendRightEquiv_symm (a : F.extendRight M) :
62+
algebraMap F M ((extendRightEquiv F M).symm a) = a := by
63+
rw [← algebraMap_extendRightEquiv, AlgEquiv.apply_symm_apply, algebraMap_apply]
64+
65+
namespace extendRight
66+
67+
variable {R S : Type*} [CommRing R] [CommRing S] [Algebra S F]
68+
69+
variable [Algebra S M] [IsScalarTower S F M]
70+
71+
theorem algebraMap_mem (s : S) : algebraMap S M s ∈ F.extendRight M := by
72+
rw [IsScalarTower.algebraMap_apply S F M, IsScalarTower.algebraMap_apply F L M]
73+
exact ⟨algebraMap F L (algebraMap S F s), by simp, rfl⟩
74+
75+
instance : SMul S (F.extendRight M) where
76+
smul s x := by
77+
refine ⟨s • x, ?_⟩
78+
rw [Algebra.smul_def]
79+
exact (F.extendRight M).mul_mem (algebraMap_mem F M s) x.prop
80+
81+
@[simp]
82+
theorem coe_smul (s : S) (x : F.extendRight M) :
83+
(s • x : F.extendRight M) = s • (x : M) := rfl
84+
85+
-- The algebra instance is defined this way to avoid diamonds, see below
86+
noncomputable instance algebra : Algebra S (F.extendRight M) where
87+
algebraMap := (algebraMap S M).codRestrict (F.extendRight M).toSubalgebra (algebraMap_mem F M ·)
88+
commutes' _ _ := Subtype.ext <| by simp [Algebra.commutes]
89+
smul_def' s x := Subtype.ext <| by
90+
convert_to s • (x : M) = _
91+
rw [MulMemClass.coe_mul, RingHom.codRestrict_apply, ← Algebra.smul_def]
92+
93+
-- Check there is no diamond
94+
example [Algebra S K] [IsScalarTower S K M] :
95+
((F.extendRight M).algebra' : Algebra S (F.extendRight M)) =
96+
(algebra F M : Algebra S (F.extendRight M)) := by
97+
with_reducible_and_instances rfl
98+
99+
instance : IsScalarTower S (F.extendRight M) M := IsScalarTower.of_algebraMap_eq' rfl
100+
101+
instance : IsScalarTower S F (F.extendRight M) := IsScalarTower.to₁₂₃ S F (F.extendRight M) M
102+
103+
instance [Algebra R S] [Algebra R F] [Algebra R M] [IsScalarTower R F M] [IsScalarTower R S M] :
104+
IsScalarTower R S (F.extendRight M) :=
105+
IsScalarTower.to₁₂₃ R S (F.extendRight M) M
106+
107+
variable (S)
108+
109+
/--
110+
Variant of `extendRightEquiv` giving an `S`-algebra isomorphism `F ≃ₐ[S] F.extendRight M`,
111+
for a commutative ring `S` with `Algebra S F`.
112+
-/
113+
noncomputable def _root_.IntermediateField.extendRightEquiv' : F ≃ₐ[S] (F.extendRight M) :=
114+
AlgEquiv.ofBijective (Algebra.algHom S F (F.extendRight M)) (extendRightEquiv F M).bijective
115+
116+
@[simp]
117+
theorem coe_extendRightEquiv' (a : F) :
118+
(extendRightEquiv' F M S a : M) = algebraMap F M a := rfl
119+
120+
@[simp]
121+
theorem algebraMap_extendRightEquiv' (a : F) :
122+
algebraMap (F.extendRight M) M (extendRightEquiv' F M S a) = algebraMap F M a := rfl
123+
124+
@[simp]
125+
theorem algebraMap_extendRightEquiv'_symm (a : F.extendRight M) :
126+
algebraMap F M ((extendRightEquiv' F M S).symm a) = a := by
127+
rw [← algebraMap_extendRightEquiv' F M S, AlgEquiv.apply_symm_apply, algebraMap_apply]
128+
129+
variable {S}
130+
131+
instance isFractionRing [IsFractionRing S F] :
132+
IsFractionRing S (F.extendRight M) :=
133+
.of_algEquiv (R := S) (L := F.extendRight M) (K := F) <| F.extendRightEquiv' M S
134+
135+
instance isIntegralClosure [Algebra R F] [Algebra R M] [IsScalarTower R F M]
136+
[IsIntegralClosure S R F] :
137+
IsIntegralClosure S R (F.extendRight M) := by
138+
refine .of_algEquiv S (F.extendRightEquiv' M R) fun x ↦ ?_
139+
rw [Subtype.ext_iff, ← algebraMap_apply (F.extendRight M), ← algebraMap_apply (F.extendRight M),
140+
algebraMap_extendRightEquiv', ← IsScalarTower.algebraMap_apply,
141+
← IsScalarTower.algebraMap_apply]
142+
143+
end IntermediateField.extendRight

‎Mathlib/RingTheory/Localization/FractionRing.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,11 @@ abbrev IsFractionRing (R : Type*) [CommSemiring R] (K : Type*) [CommSemiring K]
5555
instance {R : Type*} [Field R] : IsFractionRing R R :=
5656
IsLocalization.at_units _ (fun _ ↦ isUnit_of_mem_nonZeroDivisors)
5757

58+
theorem IsFractionRing.of_algEquiv {R : Type*} [CommSemiring R] {K L : Type*}
59+
[CommSemiring K] [Algebra R K] [CommSemiring L] [Algebra R L] [h : IsFractionRing R K]
60+
(e : K ≃ₐ[R] L) :
61+
IsFractionRing R L := IsLocalization.isLocalization_of_algEquiv _ e
62+
5863
/-- The cast from `Int` to `Rat` as a `FractionRing`. -/
5964
instance Rat.isFractionRing : IsFractionRing ℤ ℚ where
6065
map_units := by

0 commit comments

Comments
 (0)
⚡