NYLL
Module

UnramifiedCoprimality.lean

Nyll.EtaleFundamentalGroups.Kummer.Lattices.UnramifiedCoprimality
2 declarations indexed from sourceView source ↗

Module documentation

Coprimality for formally unramified finite lattice covers

A formally unramified finite-index lattice cover produces synchronized Smith coordinates with unit exponents. Every subgroup of the lattice quotient therefore embeds in a product of cyclic groups of unit orders, so its order is a unit in the coefficient ring and is prime to every residue characteristic.

Imports3
Imported by2

Declarations

theorem

isUnit_natCard_subgroup_of_formallyUnramified_latticeCover

L28 ↗
EtaleFundamentalGroups.Kummer.isUnit_natCard_subgroup_of_formallyUnramified_latticeCover
Documentation

The order of every subgroup of the quotient lattice is a unit in the coefficient ring when the associated lattice cover is formally unramified.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u uk
Lean source · statement
theorem isUnit_natCard_subgroup_of_formallyUnramified_latticeCover
    {R L : Type u} [CommRing R] [Nontrivial R]
    [AddCommGroup L] [Module.Free ℤ L] [Module.Finite ℤ L]
    (H : Submodule ℤ L) [Finite (L ⧸ H)]
    (hFU : (AddMonoidAlgebra.mapDomainRingHom R
      H.subtype.toAddMonoidHom).FormallyUnramified)
    (N : AddSubgroup (L ⧸ H)) :
    IsUnit (Nat.card N : R)
theorem

natCoprime_natCard_subgroup_of_formallyUnramified_latticeCover

L50 ↗
EtaleFundamentalGroups.Kummer.natCoprime_natCard_subgroup_of_formallyUnramified_latticeCover
Documentation

The order of every subgroup of the quotient lattice is prime to a residue characteristic when the associated monoid-algebra cover is formally unramified. The cyclic coordinates and their unit orders are constructed inside the proof; no character injection or cardinality comparison is an input.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u uk
Lean source · statement
theorem natCoprime_natCard_subgroup_of_formallyUnramified_latticeCover
    {R L : Type u} {k : Type uk}
    [CommRing R] [Nontrivial R]
    [AddCommGroup L] [Module.Free ℤ L] [Module.Finite ℤ L]
    (H : Submodule ℤ L) [Finite (L ⧸ H)]
    (hFU : (AddMonoidAlgebra.mapDomainRingHom R
      H.subtype.toAddMonoidHom).FormallyUnramified)
    (N : AddSubgroup (L ⧸ H))
    [CommRing k] [Nontrivial k]
    (φ : R →+* k) (p : ℕ) [CharP k p] (hp : p.Prime) :
    Nat.Coprime (Nat.card N) p

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