Nyll.EtaleFundamentalGroups.StrictHenselian.NormalizationPrimeInertiaFixedImage

Module documentation

Original normalization inertia fixes the actual stalk image

The target is the literal prime localization of the original integral closure. Its strict Henselian properties have already been constructed. The original inertia element supplies an actual native local automorphism with the proved base and residue squares, so the existing stalk rigidity theorem fixes the constructed map. No fixed-image or comparison premise is introduced; the reverse image and ambient fraction-field identifications remain separate.

theorem

normalizationPrimeInertia_comp_geometricStalkMap

L40 ↗

EtaleFundamentalGroups.StrictHenselian.normalizationPrimeInertia_comp_geometricStalkMap

Documentation

Every original normalization inertia element fixes the actual geometric-stalk map into the literal prime localization.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v
attribute [local instance] normalizationInertiaImageAction

Lean source · full declaration

theorem normalizationPrimeInertia_comp_geometricStalkMap
    (A : Type u) (K : Type v) (L : Type u)
    [CommRing A] [IsDomain 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.IsPrime]
    (σ : Gal(L/K)) (hσ : σ ∈ Q.inertia Gal(L/K)) :
    let : HenselianLocalRing (Localization.AtPrime Q) :=
      (integralClosure_localizationAtPrime_strictHenselian A K L Q).1
    let : IsSepClosed (IsLocalRing.ResidueField (Localization.AtPrime Q)) :=
      (integralClosure_localizationAtPrime_strictHenselian A K L Q).2
    (normalizationPrimeInertiaRingEquiv A K L Q σ hσ).toRingHom.comp
        (geometricStalkToHenselian (integralClosurePrimeBaseMap A L Q)) =
      geometricStalkToHenselian (integralClosurePrimeBaseMap A L Q) := by
  intro actualHenselian actualSepClosed
  exact geometricStalkToHenselian_comp_endomorphism (integralClosurePrimeBaseMap A L Q)
    (normalizationPrimeInertiaRingEquiv A K L Q σ hσ).toRingHom
    (normalizationPrimeInertiaRingEquiv_comp_baseMap A K L Q σ hσ)
    (normalizationPrimeInertiaRingEquiv_comp_residue A K L Q σ hσ)

Module documentation

Original normalization inertia fixes the actual stalk image

Declarations

normalizationPrimeInertia_comp_geometricStalkMap