NYLL
Module

ActualFiniteInertiaResidue.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteInertiaResidue
2 declarations indexed from sourceView source ↗

Module documentation

Residue triviality of localized finite inertia

Shows that a coefficient map satisfying the inertia difference condition becomes residue-trivial after localization, and applies this to the finite inertia action.

Imports8
Imported by2

Declarations

theorem

localRingHom_comp_residue_of_sub_mem

L34 ↗
EtaleFundamentalGroups.Inertia.localRingHom_comp_residue_of_sub_mem
Documentation

Localization of a residue-trivial coefficient map is residue-trivial. This is the coefficient argument used by individual inertia localization, with no group or automorphism dictionary in its interface.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
theorem localRingHom_comp_residue_of_sub_mem
    (B : Type w) [CommRing B] (P : Ideal B) [P.IsPrime]
    (s : B →+* B) (hP : P = P.comap s)
    (hs : ∀ b : B, s.toFun b - b ∈ P) :
    (IsLocalRing.residue (Localization.AtPrime P)).comp
        (Localization.localRingHom P P s hP) =
      IsLocalRing.residue (Localization.AtPrime P)
theorem

actualFiniteInertiaLocalRingHom_comp_residue

L64 ↗
EtaleFundamentalGroups.Inertia.actualFiniteInertiaLocalRingHom_comp_residue
Documentation

The same actual localized coefficient action fixes its residue field. The original inertia congruence supplies this fact; it is not an endpoint input.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L]
  [IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L))
Lean source · full declaration
theorem actualFiniteInertiaLocalRingHom_comp_residue [Q.IsPrime]
    (E : FiniteGaloisIntermediateField K L)
    (σ : actualNormalizationInertiaGroup A K L Q) :
    letI := finiteAbsoluteNormalizationPrime_isPrime A K L Q E
    (IsLocalRing.residue
        (Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E))).comp
        (actualFiniteInertiaLocalRingHom A K L Q E σ) =
      IsLocalRing.residue
        (Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E)) := by
  let := finiteAbsoluteNormalizationPrime_isPrime A K L Q E
  exact localRingHom_comp_residue_of_sub_mem
    (finiteAbsoluteNormalizationAlgebra A K L E)
    (finiteAbsoluteNormalizationPrime A K L Q E)
    (actualFiniteNormalizationRestrictionRingHom A K L E
      (actualNormalizationInertiaElement A K L Q σ))
    (actualFiniteNormalizationRestrictionRingHom_prime A K L Q E σ)
    (originalInertia_finiteNormalization_difference A K L Q E σ)

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