Nyll.EtaleFundamentalGroups.Kummer.Lattices.Smith.SignNormalization

Module documentation

Positive Smith coordinates for a finite-index lattice cover

The Smith coefficients produced for an integer lattice are nonzero integers. Changing the sign of each negative target coordinate replaces them by their positive natural absolute values. Functoriality of additive monoid algebras preserves the resulting coordinate square.

theorem

exists_smithNatDiagonal_monoidAlgebra

L31 ↗

EtaleFundamentalGroups.Kummer.exists_smithNatDiagonal_monoidAlgebra

Documentation

A finite-index sublattice admits Smith coordinates whose diagonal entries are positive natural numbers. The sign changes are produced from the Smith coefficients themselves, the quotient is identified with the corresponding product of cyclic groups, and the induced monoid-algebra square remains commutative. All three outputs use one canonical Smith choice.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v

Lean source · statement

theorem exists_smithNatDiagonal_monoidAlgebra
    {R : Type u} {L : Type v} [CommSemiring R] [AddCommGroup L]
    [Module.Free ℤ L] [Module.Finite ℤ L]
    (H : Submodule ℤ L) [Finite (L ⧸ H)] :
    ∃ (ι : Type v) (_ : Fintype ι) (n : ι → ℕ),
      (∀ i, 0 < n i) ∧
        ∃ (eH : H ≃+ (ι → ℤ)) (eL : L ≃+ (ι → ℤ))
          (d : (ι → ℤ) →+ (ι → ℤ))
          (_eQ : (L ⧸ H) ≃+ ∀ i, ZMod (n i)),
          (∀ x i, d x i = (n i : ℤ) * x i) ∧
            (AddMonoidAlgebra.domCongr R R eL).toAlgHom.comp
                (AddMonoidAlgebra.mapDomainAlgHom R R H.subtype.toAddMonoidHom) =
              (AddMonoidAlgebra.mapDomainAlgHom R R d).comp
                (AddMonoidAlgebra.domCongr R R eH).toAlgHom

Module documentation

Positive Smith coordinates for a finite-index lattice cover

Declarations

exists_smithNatDiagonal_monoidAlgebra