EtaleFundamentalGroups.StrictHenselian.originalFractionAbsoluteGaloisHom_ker_eq_normalClosureInertia
The canonical original fraction-point map has kernel the closed normal subgroup generated by the original normalization inertia.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v
attribute [local instance] normalizationInertiaImageAction
variable (A : Type u) (K : Type v) (L : Type u)
[CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A]
[Field K] [Field L] [Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L] [IsSepClosed L]
(Q : Ideal (integralClosure A L)) [Q.IsMaximal]Lean source · full declaration
theorem originalFractionAbsoluteGaloisHom_ker_eq_normalClosureInertia :
let : FaithfulSMul A L :=
(Module.isTorsionFree_iff_faithfulSMul (R := A) (A := L)).mp
(Module.IsTorsionFree.trans_faithfulSMul A K L)
let : Algebra (FractionRing A) K := FractionRing.liftAlgebra A K
let : Algebra (FractionRing A) L := FractionRing.liftAlgebra A L
let : IsSepClosure (FractionRing A) L := originalFractionField_isSepClosure A K L
(originalFractionAbsoluteGaloisHom A K L).toMonoidHom.ker =
ProCGroups.Presentations.Subgroup.closedNormalClosure
(Q.inertia Gal(L/K) : Set Gal(L/K)) := by
intro actualFaithful actualFractionAlgebra actualAmbientAlgebra actualSepClosure
let : Algebra.IsAlgebraic A L :=
(IsFractionRing.comap_isAlgebraic_iff (A := A) (K := K) (C := L)).mpr inferInstance
let : HenselianLocalRing (Localization.AtPrime Q) :=
(integralClosure_primeLocalization_strictHenselian_of_algebraic A L Q).1
let : IsSepClosed (IsLocalRing.ResidueField (Localization.AtPrime Q)) :=
(integralClosure_primeLocalization_strictHenselian_of_algebraic A L Q).2
let ψ := (IsLocalRing.residue (Localization.AtPrime Q)).comp
(integralClosurePrimeBaseMap A L Q)
let : IsLocalHom ψ := normalizationResiduePoint_isLocalHom A L Q
let E := FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom ψ)))
let : Algebra K E := (normalizationStalkFractionBaseMap A K L Q).toAlgebra
let : Algebra E L := (geometricStalkFractionToNormalizationField A L Q).toAlgebra
let : IsScalarTower K E L := normalizationStalkFractionField_isScalarTower A K L Q
let : IsSepClosure E L := normalizationStalkFractionField_isSepClosure A K L Q
let : Algebra (FractionRing A) E := (geometricStalkFractionFieldMap ψ).toAlgebra
let : IsScalarTower (FractionRing A) E L :=
normalizationStalkFractionField_isScalarTower A (FractionRing A) L Q
let comparison :=
((fieldBasePointFiberIso (FractionRing A) E L).conjAut.trans
(MulAut.conj (fieldFundamentalGroupComparisonAut (FractionRing A) E L))).trans
((absoluteGaloisToFiberAutMulEquiv (FractionRing A) L inferInstance).symm.trans
(originalFractionFieldGaloisEquiv A K L))
let r := Spec.map (CommRingCat.ofHom (algebraMap A (FractionRing A)))
let quotient := (fundamentalGroupHom r
(ξ E L ≫ ξ (FractionRing A) E)).toMonoidHom.comp comparison.symm.toMonoidHom
let T := fieldSourceComparisonFiberIso (FractionRing A) E L r
let originalEquiv := originalFractionFieldGaloisEquiv A K L
let sourceComparison :=
((fieldBasePointFiberIso (FractionRing A) E L).conjAut.trans
(MulAut.conj (fieldFundamentalGroupComparisonAut (FractionRing A) E L))).trans
(absoluteGaloisToFiberAutMulEquiv (FractionRing A) L inferInstance).symm
have hq (σ : Gal(L/K)) : T.conjAut (quotient σ) =
originalFractionAbsoluteGaloisHom A K L σ := by
have hsource : sourceComparison (comparison.symm σ) = originalEquiv.symm σ := by
have h := congrArg originalEquiv.symm (comparison.apply_symm_apply σ)
change originalEquiv.symm
(originalEquiv (sourceComparison (comparison.symm σ))) = originalEquiv.symm σ at h
rw [originalEquiv.symm_apply_apply] at h
exact h
have h := fieldSourceAbsoluteGaloisHom_comparison
(FractionRing A) E L r (comparison.symm σ)
exact h.trans (congrArg (fieldSourceAbsoluteGaloisHom (FractionRing A) L r) hsource)
have hker : quotient.ker = ProCGroups.Presentations.Subgroup.closedNormalClosure
(Q.inertia Gal(L/K) : Set Gal(L/K)) :=
(originalInertia_normalLocal_exactSequence A K L Q).2.2
calc
(originalFractionAbsoluteGaloisHom A K L).toMonoidHom.ker = quotient.ker := by
ext σ
change originalFractionAbsoluteGaloisHom A K L σ = 1 ↔ quotient σ = 1
constructor
· intro h
apply T.conjAut.injective
rw [hq, h, map_one]
· intro h
rw [← hq, h, map_one]
_ = ProCGroups.Presentations.Subgroup.closedNormalClosure
(Q.inertia Gal(L/K) : Set Gal(L/K)) := hker