LocalClassFieldTheory.intrinsicExtensionSubgroup_iff_ambientEmbeddedField
Under the embedded-field base equivalence, membership in the intrinsic extension subgroup for E / F is equivalent to membership in the ambient extension subgroup determined by the two field ranges.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRelLean source · full declaration
theorem
intrinsicExtensionSubgroup_iff_ambientEmbeddedField
(K F E : Type) [Field K] [Field F] [Field E]
[Algebra K F] [Algebra F E] [Algebra K E]
[IsScalarTower K F E]
[FiniteDimensional K F] [Algebra.IsSeparable K F]
[FiniteDimensional F E] [IsGalois F E]
(j : E →ₐ[K] SeparableClosure K) :
let i :=
j.comp (IsScalarTower.toAlgHom K F E)
letI : Algebra F (SeparableClosure F) :=
(separableClosure F (AlgebraicClosure F)).algebra
letI : Algebra F (SeparableClosure K) :=
i.toRingHom.toAlgebra
∀ (e : SeparableClosure F ≃ₐ[F] SeparableClosure K)
(tau : (intrinsicAbstractBase F).toSubgroup),
let jF : E →ₐ[F] SeparableClosure K :=
{ j with commutes' := fun x => rfl }
let jI : E →ₐ[F] SeparableClosure F :=
e.symm.toAlgHom.comp jF
let EI :=
finiteGaloisAbstractExtensionOfEmbedding F E jI
let H₀ :=
closedFixingSubgroup K (SeparableClosure K)
(AlgHom.fieldRange i)
let J₀ :=
closedFixingSubgroup K (SeparableClosure K)
(AlgHom.fieldRange j)
let hJH : J₀.toSubgroup ≤ H₀.toSubgroup := by
change
(AlgHom.fieldRange j).fixingSubgroup ≤
(AlgHom.fieldRange i).fixingSubgroup
apply (AlgHom.fieldRange i).fixingSubgroup_le
intro x hx
rcases hx with ⟨y, rfl⟩
exact ⟨algebraMap F E y, rfl⟩
tau ∈ extensionSubgroup
(intrinsicAbstractBase F) EI.field EI.below ↔
intrinsicBaseEquivAmbientEmbeddedField K F i e tau ∈
extensionSubgroup H₀ J₀ hJH := by
dsimp only
let i :=
j.comp (IsScalarTower.toAlgHom K F E)
let : Algebra F (SeparableClosure K) :=
i.toRingHom.toAlgebra
intro e tau
let jF : E →ₐ[F] SeparableClosure K :=
{ j with commutes' := fun x => rfl }
let jI : E →ₐ[F] SeparableClosure F :=
e.symm.toAlgHom.comp jF
let EI :=
finiteGaloisAbstractExtensionOfEmbedding F E jI
let H₀ :=
closedFixingSubgroup K (SeparableClosure K)
(AlgHom.fieldRange i)
let J₀ :=
closedFixingSubgroup K (SeparableClosure K)
(AlgHom.fieldRange j)
let hJH : J₀.toSubgroup ≤ H₀.toSubgroup := by
change
(AlgHom.fieldRange j).fixingSubgroup ≤
(AlgHom.fieldRange i).fixingSubgroup
apply (AlgHom.fieldRange i).fixingSubgroup_le
intro x hx
rcases hx with ⟨y, rfl⟩
exact ⟨algebraMap F E y, rfl⟩
change
tau.1 ∈ (AlgHom.fieldRange jI).fixingSubgroup ↔
(intrinsicBaseEquivAmbientEmbeddedField
K F i e tau).1 ∈
(AlgHom.fieldRange j).fixingSubgroup
rw [IntermediateField.mem_fixingSubgroup_iff,
IntermediateField.mem_fixingSubgroup_iff]
constructor
· intro htau x hx
obtain ⟨y, rfl⟩ := hx
change
(intrinsicBaseEquivAmbientEmbeddedField
K F i e tau).1.1 (j y) = j y
rw [
intrinsicBaseEquivAmbientEmbeddedField_apply_val
K F i e tau]
change e (tau.1 (jI y)) = j y
rw [htau (jI y) ⟨y, rfl⟩]
exact e.apply_symm_apply (j y)
· intro hpsi x hx
obtain ⟨y, rfl⟩ := hx
apply e.injective
change
e (tau.1 (e.symm (j y))) =
e (e.symm (j y))
rw [e.apply_symm_apply]
rw [← intrinsicBaseEquivAmbientEmbeddedField_apply_val
K F i e tau]
exact hpsi (j y) ⟨y, rfl⟩