NYLL
Module

OriginalInertiaLocalExactSequence.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.OriginalInertiaLocalExactSequence
2 declarations indexed from sourceView source ↗

Module documentation

The original inertia presentation of the normal-local fundamental group

The actual normal-local strict-generic sequence is transported through the proved comparison with the original ambient Galois group. This gives the literal fraction-pullback quotient map, with its kernel generated as a closed normal subgroup by the original normalization inertia.

Imports5
Imported by2

Declarations

theorem

map_closedNormalClosure_of_isHomeomorph

L35 ↗
EtaleFundamentalGroups.StrictHenselian.map_closedNormalClosure_of_isHomeomorph
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v
attribute [local instance] normalizationInertiaImageAction
Lean source · statement
theorem map_closedNormalClosure_of_isHomeomorph
    {G H : Type*} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H]
    [IsTopologicalGroup G] [IsTopologicalGroup H]
    (e : G ≃* H) (he : IsHomeomorph e) (s : Set G) :
    (ProCGroups.Presentations.Subgroup.closedNormalClosure s).map e.toMonoidHom =
      ProCGroups.Presentations.Subgroup.closedNormalClosure (e '' s)
theorem

originalInertia_normalLocal_exactSequence

L52 ↗
EtaleFundamentalGroups.StrictHenselian.originalInertia_normalLocal_exactSequence
Documentation

The original absolute Galois group maps continuously and surjectively to the fundamental group of the original local ring. The map is the actual fraction-field pullback map under the explicit geometric-fiber comparison, and its kernel is the closed normal subgroup generated by original inertia.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v
attribute [local instance] normalizationInertiaImageAction
Lean source · full declaration
theorem originalInertia_normalLocal_exactSequence
    (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] :
    let : Algebra.IsAlgebraic A L :=
      (IsFractionRing.comap_isAlgebraic_iff (A := A) (K := K) (C := L)).mpr inferInstance
    let : FaithfulSMul A L :=
      (Module.isTorsionFree_iff_faithfulSMul (R := A) (A := L)).mp
        (Module.IsTorsionFree.trans_faithfulSMul A K L)
    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) K := FractionRing.liftAlgebra A K
    let : Algebra (FractionRing A) L := FractionRing.liftAlgebra A L
    let : IsSepClosure (FractionRing A) L := originalFractionField_isSepClosure A K L
    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
    Function.Surjective quotient ∧ Continuous quotient ∧
      quotient.ker = ProCGroups.Presentations.Subgroup.closedNormalClosure
        (Q.inertia Gal(L/K) : Set Gal(L/K)) := by
  intro actualAlgebraic actualFaithful actualHenselian actualResidueSepClosed
    ψ actualLocal E actualBaseAlgebra actualAmbientAlgebra actualTower actualSepClosure
    actualFractionAlgebra actualFractionAmbientAlgebra actualFractionSepClosure
    actualCanonicalBaseAlgebra actualCanonicalTower comparison r quotient
  let absoluteEquiv := absoluteGaloisToFiberAutMulEquiv (FractionRing A) L
    (inferInstance : IsSepClosed L)
  have habsolute : Continuous absoluteEquiv :=
    (toAutMulEquiv_isHomeomorph (fib (FractionRing A) L) Gal(L/FractionRing A)).continuous
  have habsoluteInv : Continuous absoluteEquiv.symm :=
    Continuous.continuous_symm_of_equiv_compact_to_t2
      (f := absoluteEquiv.toEquiv) habsolute
  have hcomparison : Continuous comparison :=
    (originalFractionFieldGaloisEquiv_continuous A K L).comp
      (habsoluteInv.comp
        ((IsTopologicalGroup.continuous_conj
          (fieldFundamentalGroupComparisonAut (FractionRing A) E L)).comp
            (continuous_conjAut (fieldBasePointFiberIso (FractionRing A) E L))))
  have hcomparisonHomeo : IsHomeomorph comparison := by
    rw [isHomeomorph_iff_continuous_bijective]
    exact ⟨hcomparison, comparison.bijective⟩
  have hcomparisonInv : Continuous comparison.symm :=
    Continuous.continuous_symm_of_equiv_compact_to_t2
      (f := comparison.toEquiv) hcomparison
  have hsequence := geometricStalk_normalLocal_exactSequence ψ (ξ E L)
  have hsurjective : Function.Surjective
      (fundamentalGroupHom r (ξ E L ≫ ξ (FractionRing A) E)) := hsequence.1
  have hkernel :
      (fundamentalGroupHom r (ξ E L ≫ ξ (FractionRing A) E)).toMonoidHom.ker =
        ProCGroups.Presentations.Subgroup.closedNormalClosure
          (Set.range (fundamentalGroupHom (ξ (FractionRing A) E) (ξ E L))) := hsequence.2.2
  have hrange : (comparison.toMonoidHom.comp
      (fundamentalGroupHom (ξ (FractionRing A) E) (ξ E L)).toMonoidHom).range =
        Q.inertia Gal(L/K) := geometricStalkFundamentalGroup_originalInertia_range A K L Q
  have himage : comparison '' Set.range
      (fundamentalGroupHom (ξ (FractionRing A) E) (ξ E L)) =
        (Q.inertia Gal(L/K) : Set Gal(L/K)) := by
    rw [← Set.range_comp]
    exact congrArg (fun H : Subgroup Gal(L/K) => (H : Set Gal(L/K))) hrange
  refine ⟨hsurjective.comp comparison.symm.surjective,
    (fundamentalGroupHom r (ξ E L ≫ ξ (FractionRing A) E)).continuous.comp
      hcomparisonInv, ?_⟩
  change ((fundamentalGroupHom r
    (ξ E L ≫ ξ (FractionRing A) E)).toMonoidHom.comp comparison.symm.toMonoidHom).ker = _
  calc
    ((fundamentalGroupHom r (ξ E L ≫ ξ (FractionRing A) E)).toMonoidHom.comp
        comparison.symm.toMonoidHom).ker =
      (fundamentalGroupHom r (ξ E L ≫ ξ (FractionRing A) E)).toMonoidHom.ker.map
        comparison.toMonoidHom :=
      MonoidHom.ker_comp_mulEquiv
        (fundamentalGroupHom r (ξ E L ≫ ξ (FractionRing A) E)).toMonoidHom comparison.symm
    _ = (ProCGroups.Presentations.Subgroup.closedNormalClosure
        (Set.range (fundamentalGroupHom (ξ (FractionRing A) E) (ξ E L)))).map
          comparison.toMonoidHom := congrArg (Subgroup.map comparison.toMonoidHom) hkernel
    _ = ProCGroups.Presentations.Subgroup.closedNormalClosure
        (comparison '' Set.range (fundamentalGroupHom (ξ (FractionRing A) E) (ξ E L))) :=
      map_closedNormalClosure_of_isHomeomorph comparison hcomparisonHomeo _
    _ = ProCGroups.Presentations.Subgroup.closedNormalClosure
        (Q.inertia Gal(L/K) : Set Gal(L/K)) :=
      congrArg ProCGroups.Presentations.Subgroup.closedNormalClosure himage

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.