Module

Coprimality.lean

Nyll.EtaleFundamentalGroups.Kummer.Boundary.Lattice.Coprimality

2 declarations indexed from sourceView source ↗

Module documentation

Coprimality for a lattice cover on a boundary complement

For a finite lattice cover over the complement of a prime normal-crossings boundary, formal unramifiedness makes every quotient subgroup order a unit on the complement. Componentwise characteristic zero then reflects that unit to the original ring, where any characteristic-p specialization detects coprimality.

Imports2

Imported by2

theorem

isUnit_natCard_subgroup_of_formallyUnramified_boundaryLatticeCover

L30 ↗

EtaleFundamentalGroups.Kummer.isUnit_natCard_subgroup_of_formallyUnramified_boundaryLatticeCover

Documentation

Every subgroup of a formally unramified lattice cover on a full prime boundary complement has unit order in the original ring.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open scoped BigOperators
universe uR uS uk

Lean source · statement

theorem isUnit_natCard_subgroup_of_formallyUnramified_boundaryLatticeCover
    {R : Type uR} {S L : Type uS}
    [CommRing R] [IsDomain R] [CommRing S] [Algebra R S]
    {ι : Type*} (s : Finset ι) (t : ι → R)
    [IsLocalization.Away (∏ i ∈ s, t i) S]
    (ht : ∀ i ∈ s, Prime (t i))
    (hCharZero : ∀ i ∈ s, CharZero (R ⧸ Ideal.span {t i}))
    [AddCommGroup L] [Module.Free ℤ L] [Module.Finite ℤ L]
    (H : Submodule ℤ L) [Finite (L ⧸ H)]
    (hFU : (AddMonoidAlgebra.mapDomainRingHom S
      H.subtype.toAddMonoidHom).FormallyUnramified)
    (N : AddSubgroup (L ⧸ H)) :
    IsUnit (Nat.card N : R)

theorem

natCoprime_natCard_subgroup_of_formallyUnramified_boundaryLatticeCover

L58 ↗

EtaleFundamentalGroups.Kummer.natCoprime_natCard_subgroup_of_formallyUnramified_boundaryLatticeCover