Adjoining Elements to Fields #
In this file we introduce the notion of adjoining elements to fields.
This isn't quite the same as adjoining elements to rings.
For example, Algebra.adjoin K {x} might not include x⁻¹.
Notation #
F⟮α⟯: adjoin a single elementαtoF(in scopeIntermediateField).
def
IntermediateField.adjoin
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S : Set E)
:
adjoin F S extends a field F by adjoining a set S ⊆ E.
Stacks Tag 09FZ (first part)
Equations
- IntermediateField.adjoin F S = { toSubsemiring := (Subfield.closure (Set.range ⇑(algebraMap F E) ∪ S)).toSubsemiring, algebraMap_mem' := ⋯, inv_mem' := ⋯ }
Instances For
@[simp]
theorem
IntermediateField.adjoin_toSubfield
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S : Set E)
:
(adjoin F S).toSubfield = Subfield.closure (Set.range ⇑(algebraMap F E) ∪ S)
theorem
IntermediateField.gc
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
:
GaloisConnection (adjoin F) fun (x : IntermediateField F E) => ↑x
def
IntermediateField.gi
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
:
GaloisInsertion (adjoin F) fun (x : IntermediateField F E) => ↑x
Galois insertion between adjoin and coe.
Equations
- IntermediateField.gi = { choice := fun (s : Set E) (hs : ↑(IntermediateField.adjoin F s) ≤ s) => (IntermediateField.adjoin F s).copy s ⋯, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
Instances For
instance
IntermediateField.instCompleteLattice
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
:
Equations
- IntermediateField.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
theorem
IntermediateField.sSup_def
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S : Set (IntermediateField F E))
:
instance
IntermediateField.instInhabited
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
:
Inhabited (IntermediateField F E)
Equations
- IntermediateField.instInhabited = { default := ⊤ }
Equations
- IntermediateField.instUnique = { toInhabited := inferInstanceAs (Inhabited (IntermediateField F F)), uniq := ⋯ }
theorem
IntermediateField.bot_toSubfield
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
:
⊥.toSubfield = (algebraMap F E).fieldRange
@[simp]
theorem
IntermediateField.coe_sInf
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S : Set (IntermediateField F E))
:
↑(sInf S) = sInf ((fun (x : IntermediateField F E) => ↑x) '' S)
@[simp]
theorem
IntermediateField.sInf_toSubalgebra
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S : Set (IntermediateField F E))
:
(sInf S).toSubalgebra = sInf (toSubalgebra '' S)
@[simp]
theorem
IntermediateField.sInf_toSubfield
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S : Set (IntermediateField F E))
:
(sInf S).toSubfield = sInf (toSubfield '' S)
@[simp]
theorem
IntermediateField.sSup_toSubfield
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S : Set (IntermediateField F E))
(hS : S.Nonempty)
:
(sSup S).toSubfield = sSup (toSubfield '' S)
def
IntermediateField.equivOfEq
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{S T : IntermediateField F E}
(h : S = T)
:
Construct an algebra isomorphism from an equality of intermediate fields
Equations
- IntermediateField.equivOfEq h = S.equivOfEq T.toSubalgebra ⋯
Instances For
@[simp]
theorem
IntermediateField.equivOfEq_rfl
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S : IntermediateField F E)
:
noncomputable def
IntermediateField.botEquiv
(F : Type u_1)
[Field F]
(E : Type u_2)
[Field E]
[Algebra F E]
:
The bottom intermediate_field is isomorphic to the field.
Equations
- IntermediateField.botEquiv F E = (⊥.equivOfEq ⊥ ⋯).trans (Algebra.botEquiv F E)
Instances For
noncomputable instance
IntermediateField.algebraOverBot
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
:
Equations
- IntermediateField.algebraOverBot = (↑(IntermediateField.botEquiv F E)).toAlgebra
instance
IntermediateField.isScalarTower_over_bot
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
:
IsScalarTower (↥⊥) F E
The top IntermediateField is isomorphic to the field.
This is the intermediate field version of Subalgebra.topEquiv.
Instances For
@[simp]
theorem
IntermediateField.restrictScalars_bot_eq_self
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(K : IntermediateField F E)
:
restrictScalars F ⊥ = K
theorem
IntermediateField.restrictScalars_sup
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(K : Type u_3)
[Field K]
[Algebra K E]
[Algebra K F]
[IsScalarTower K F E]
(L L' : IntermediateField F E)
:
restrictScalars K L ⊔ restrictScalars K L' = restrictScalars K (L ⊔ L')
theorem
IntermediateField.restrictScalars_inf
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(K : Type u_3)
[Field K]
[Algebra K E]
[Algebra K F]
[IsScalarTower K F E]
(L L' : IntermediateField F E)
:
restrictScalars K L ⊓ restrictScalars K L' = restrictScalars K (L ⊓ L')
noncomputable def
IntermediateField.equivMap
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{K : Type u_3}
[Field K]
[Algebra F K]
(L : IntermediateField F E)
(f : E →ₐ[F] K)
:
An intermediate field is isomorphic to its image under an AlgHom
(which is automatically injective)
Equations
- L.equivMap f = (AlgEquiv.ofInjective (f.comp L.val) ⋯).trans (IntermediateField.equivOfEq ⋯)
Instances For
instance
IntermediateField.adjoin.fieldCoe
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S : Set E)
:
Equations
- IntermediateField.adjoin.fieldCoe F S = { coe := fun (x : F) => ⟨(algebraMap F E) x, ⋯⟩ }
theorem
IntermediateField.adjoin_adjoin_comm
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S T : Set E)
:
restrictScalars F (adjoin (↥(adjoin F S)) T) = restrictScalars F (adjoin (↥(adjoin F T)) S)
F[S][T] = F[T][S]
@[simp]
theorem
IntermediateField.lift_adjoin
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(K : IntermediateField F E)
(S : Set ↥K)
:
theorem
IntermediateField.lift_adjoin_simple
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(K : IntermediateField F E)
(α : ↥K)
:
@[simp]
theorem
IntermediateField.adjoin_self
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(K : IntermediateField F E)
:
theorem
IntermediateField.restrictScalars_adjoin
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(K : IntermediateField F E)
(S : Set E)
:
restrictScalars F (adjoin (↥K) S) = adjoin F (↑K ∪ S)
theorem
IntermediateField.extendScalars_adjoin
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{K : IntermediateField F E}
{S : Set E}
(h : K ≤ adjoin F S)
:
extendScalars h = adjoin (↥K) S
theorem
IntermediateField.restrictScalars_adjoin_eq_sup
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(K : IntermediateField F E)
(S : Set E)
:
restrictScalars F (adjoin (↥K) S) = K ⊔ adjoin F S
theorem
IntermediateField.restrictScalars_adjoin_of_algEquiv
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{L : Type u_3}
{L' : Type u_4}
[Field L]
[Field L']
[Algebra F L]
[Algebra L E]
[Algebra F L']
[Algebra L' E]
[IsScalarTower F L E]
[IsScalarTower F L' E]
(i : L ≃ₐ[F] L')
(hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i)
(S : Set E)
:
restrictScalars F (adjoin L S) = restrictScalars F (adjoin L' S)
If E / L / F and E / L' / F are two field extension towers, L ≃ₐ[F] L' is an isomorphism
compatible with E / L and E / L', then for any subset S of E, L(S) and L'(S) are
equal as intermediate fields of E / F.
theorem
IntermediateField.adjoin_induction
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{s : Set E}
{p : (x : E) → x ∈ adjoin F s → Prop}
(mem : ∀ (x : E) (hx : x ∈ s), p x ⋯)
(algebraMap : ∀ (x : F), p ((algebraMap F E) x) ⋯)
(add : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x + y) ⋯)
(inv : ∀ (x : E) (hx : x ∈ adjoin F s), p x hx → p x⁻¹ ⋯)
(mul : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x * y) ⋯)
{x : E}
(h : x ∈ adjoin F s)
:
p x h
If x₁ x₂ ... xₙ : E then F⟮x₁,x₂,...,xₙ⟯ is the IntermediateField F E
generated by these elements.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
IntermediateField.AdjoinSimple.gen
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(α : E)
:
↥F⟮α⟯
generator of F⟮α⟯
Equations
- IntermediateField.AdjoinSimple.gen F α = ⟨α, ⋯⟩
Instances For
theorem
IntermediateField.AdjoinSimple.algebraMap_gen
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(α : E)
:
(algebraMap (↥F⟮α⟯) E) (gen F α) = α
theorem
IntermediateField.adjoin_simple_adjoin_simple
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(α β : E)
:
restrictScalars F (↥F⟮α⟯)⟮β⟯ = F⟮α, β⟯
theorem
IntermediateField.adjoin_simple_comm
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(α β : E)
:
restrictScalars F (↥F⟮α⟯)⟮β⟯ = restrictScalars F (↥F⟮β⟯)⟮α⟯
def
IntermediateField.FG
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S : IntermediateField F E)
:
An intermediate field S is finitely generated if there exists t : Finset E such that
IntermediateField.adjoin F t = S.
Stacks Tag 09FZ (second part)
Equations
- S.FG = ∃ (t : Finset E), IntermediateField.adjoin F ↑t = S
Instances For
theorem
IntermediateField.fg_sup
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{S T : IntermediateField F E}
(hS : S.FG)
(hT : T.FG)
:
(S ⊔ T).FG
theorem
IntermediateField.fg_iSup
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{ι : Sort u_3}
[Finite ι]
{S : ι → IntermediateField F E}
(h : ∀ (i : ι), (S i).FG)
:
(⨆ (i : ι), S i).FG
theorem
IntermediateField.induction_on_adjoin_finset
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S : Finset E)
(P : IntermediateField F E → Prop)
(base : P ⊥)
(ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯))
:
P (adjoin F ↑S)
theorem
IntermediateField.induction_on_adjoin_fg
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(P : IntermediateField F E → Prop)
(base : P ⊥)
(ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F (↥K)⟮x⟯))
(K : IntermediateField F E)
(hK : K.FG)
:
P K
@[simp]
@[simp]
theorem
Subfield.extendScalars_sup
{L : Type u_2}
[Field L]
{F E E' : Subfield L}
(h : F ≤ E)
(h' : F ≤ E')
:
extendScalars h ⊔ extendScalars h' = extendScalars ⋯
theorem
Subfield.extendScalars_inf
{L : Type u_2}
[Field L]
{F E E' : Subfield L}
(h : F ≤ E)
(h' : F ≤ E')
:
extendScalars h ⊓ extendScalars h' = extendScalars ⋯
@[simp]
theorem
IntermediateField.extendScalars_self
{K : Type u_1}
[Field K]
{L : Type u_2}
[Field L]
[Algebra K L]
(F : IntermediateField K L)
:
extendScalars ⋯ = ⊥
@[simp]
theorem
IntermediateField.extendScalars_top
{K : Type u_1}
[Field K]
{L : Type u_2}
[Field L]
[Algebra K L]
(F : IntermediateField K L)
:
extendScalars ⋯ = ⊤
theorem
IntermediateField.extendScalars_sup
{K : Type u_1}
[Field K]
{L : Type u_2}
[Field L]
[Algebra K L]
{F E E' : IntermediateField K L}
(h : F ≤ E)
(h' : F ≤ E')
:
extendScalars h ⊔ extendScalars h' = extendScalars ⋯
theorem
IntermediateField.extendScalars_inf
{K : Type u_1}
[Field K]
{L : Type u_2}
[Field L]
[Algebra K L]
{F E E' : IntermediateField K L}
(h : F ≤ E)
(h' : F ≤ E')
:
extendScalars h ⊓ extendScalars h' = extendScalars ⋯