Module

Coprimality.lean

Nyll.EtaleFundamentalGroups.Kummer.Lattices.Coprimality

1 declaration indexed from sourceView source ↗

Module documentation

Coprimality from a finite Kummer character lattice

An injective character-lattice map into a finite product of cyclic groups makes the lattice order divide the product of the Kummer exponents. Thus, if every exponent is a unit in the coefficient ring, the lattice order is a unit there as well.

Imports3

Mathlib.Algebra.BigOperators.Ring.Finset
Mathlib.GroupTheory.Coset.Card
Mathlib.Data.Fintype.EquivFin

Imported by3

theorem

isUnit_natCard_of_injective_pi_zmod

L33 ↗

EtaleFundamentalGroups.Kummer.isUnit_natCard_of_injective_pi_zmod

Documentation

The order of a finite additive group embedded in a product of Kummer cyclic groups is a unit whenever all Kummer exponents are units.

AddSubgroup.card_dvd_of_injective is the range-plus-Lagrange step; the cardinality of the target is then computed coordinatewise.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open scoped BigOperators
universe uR uI uN

Lean source · statement

theorem isUnit_natCard_of_injective_pi_zmod
    {R : Type uR} [CommSemiring R]
    {I : Type uI} [Finite I] (n : I → ℕ)
    {N : Type uN} [AddGroup N] [Finite N]
    (χ : N →+ ∀ i, ZMod (n i)) (hχ : Function.Injective χ)
    (hnUnit : ∀ i, IsUnit (n i : R)) :
    IsUnit (Nat.card N : R)

Module documentation

Coprimality from a finite Kummer character lattice

Declarations

isUnit_natCard_of_injective_pi_zmod