Module

FiniteIdealTameIndex.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteIdealTameIndex

4 declarations indexed from sourceView source ↗

Module documentation

The actual finite ideal tame order is an invertible base-residue exponent

The coefficient map from the original local ring into the prime localization is local because the prime lies over the maximal ideal. Hence invertibility of the actual tame order in the upper local residue reflects to the original ring and then descends to its residue field. This constructs its literal index in the full prime-to-characteristic roots system.

Imports4

Nyll.EtaleFundamentalGroups.Inertia.FiniteIdealTameOrder
Nyll.EtaleFundamentalGroups.Inertia.PrimeToRootsInverseSystem
Mathlib.RingTheory.LocalRing.RingHom.Basic
Mathlib.RingTheory.LocalRing.ResidueField.Basic

Imported by2

theorem

coefficientComposite_isLocalHom

L30 ↗

EtaleFundamentalGroups.Inertia.coefficientComposite_isLocalHom

Documentation

The original coefficient composite is local at a prime over the base maximal ideal. No A-action on the localization is installed.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

Lean source · statement

theorem coefficientComposite_isLocalHom
    (A : Type u) (B : Type v) [CommRing A] [CommRing B]
    [IsLocalRing A] [Algebra A B]
    (Q : Ideal B) [Q.IsPrime] [Q.LiesOver (IsLocalRing.maximalIdeal A)] :
    IsLocalHom ((algebraMap B (Localization.AtPrime Q)).comp (algebraMap A B))

theorem

nat_isUnit_of_isUnit_residue_of_localHom

L51 ↗

EtaleFundamentalGroups.Inertia.nat_isUnit_of_isUnit_residue_of_localHom

Documentation

Residue invertibility reflects through the actual local coefficient map, using only its ring-homomorphism data.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

Lean source · statement

theorem nat_isUnit_of_isUnit_residue_of_localHom
    {A : Type u} {R : Type v} [CommRing A] [CommRing R] [IsLocalRing R]
    (f : A →+* R) [IsLocalHom f] (n : ℕ)
    (hn : IsUnit (n : IsLocalRing.ResidueField R)) : IsUnit (n : A)

theorem

finiteIdealTameOrder_isUnit_base

L63 ↗

EtaleFundamentalGroups.Inertia.finiteIdealTameOrder_isUnit_base

Documentation

The actual finite tame order is invertible in the original local base ring. Its upper residue invertibility is supplied by the genuine character.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

Lean source · statement

theorem finiteIdealTameOrder_isUnit_base
    (A : Type u) (B : Type v) [CommRing A] [CommRing B]
    [IsLocalRing A] [Algebra A B] [IsDedekindDomain B]
    (G : Type w) [Group G] [Finite G] [MulSemiringAction G B]
    (Q : Ideal B) [Q.IsPrime] [Q.LiesOver (IsLocalRing.maximalIdeal A)]
    (hQ : Q ≠ ⊥) : IsUnit (finiteIdealTameOrder B G Q hQ : A)

def