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
Instances For
@[simp]
theorem
IntermediateField.adjoin_le_iff
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{S : Set E}
{T : IntermediateField F E}
:
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 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
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 := ⋯ }
@[simp]
theorem
IntermediateField.inf_toSubalgebra
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S T : IntermediateField F E)
:
@[simp]
theorem
IntermediateField.inf_toSubfield
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S T : IntermediateField F E)
:
@[simp]
theorem
IntermediateField.sup_toSubfield
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S T : IntermediateField F E)
:
@[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))
:
@[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))
:
@[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))
:
@[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)
:
@[simp]
theorem
IntermediateField.iInf_toSubalgebra
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{ι : Sort u_3}
(S : ι → IntermediateField F E)
:
@[simp]
theorem
IntermediateField.iInf_toSubfield
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{ι : Sort u_3}
(S : ι → IntermediateField F E)
:
@[simp]
theorem
IntermediateField.iSup_toSubfield
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{ι : Sort u_3}
[Nonempty ι]
(S : ι → IntermediateField F E)
:
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
Instances For
@[simp]
theorem
IntermediateField.equivOfEq_apply
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{S T : IntermediateField F E}
(h : S = T)
(x : ↥S.toSubalgebra)
:
@[simp]
theorem
IntermediateField.equivOfEq_symm
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{S T : IntermediateField F E}
(h : S = T)
:
@[simp]
theorem
IntermediateField.equivOfEq_rfl
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S : IntermediateField F E)
:
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)
:
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)
:
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)
:
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
Instances For
theorem
IntermediateField.adjoin_le_subfield
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(S : Set E)
{K : Subfield E}
(HF : Set.range ⇑(algebraMap F E) ⊆ ↑K)
(HS : S ⊆ ↑K)
:
If K is a field with F ⊆ K and S ⊆ K then adjoin F S ≤ K.
@[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)
:
@[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)
:
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)
:
theorem
IntermediateField.iSup_eq_adjoin
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{ι : Sort u_3}
(f : ι → IntermediateField F E)
:
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)
:
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.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)
Instances For
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
theorem
IntermediateField.map_comap_eq_self_of_surjective
{K : Type u_1}
{L : Type u_2}
{L' : Type u_3}
[Field K]
[Field L]
[Field L']
[Algebra K L]
[Algebra K L']
{f : L →ₐ[K] L'}
(hf : Function.Surjective ⇑f)
(S : IntermediateField K L')
:
@[simp]
@[simp]
@[simp]
theorem
IntermediateField.extendScalars_self
{K : Type u_1}
[Field K]
{L : Type u_2}
[Field L]
[Algebra K L]
(F : IntermediateField K L)
:
@[simp]
theorem
IntermediateField.extendScalars_top
{K : Type u_1}
[Field K]
{L : Type u_2}
[Field L]
[Algebra K L]
(F : IntermediateField K L)
: