Nyll.EtaleFundamentalGroups.Kummer.Lattices.Smith.LatticeCover

Module documentation

Smith coordinates for a finite-index lattice cover

Smith normal form gives coordinates in which a finite-index inclusion of free integer lattices is diagonal. The same Smith choice identifies the quotient with a product of cyclic groups, while functoriality of additive monoid algebras turns the inclusion into a commutative square of algebra maps.

theorem

exists_smithDiagonal_monoidAlgebra

L31 ↗

EtaleFundamentalGroups.Kummer.exists_smithDiagonal_monoidAlgebra

Documentation

A finite-index sublattice admits Smith coordinates. The induced map of additive monoid algebras is conjugate, through the coordinate equivalences, to the coordinatewise diagonal map, and the same coefficients give cyclic coordinates on the quotient lattice.

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_smithDiagonal_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 ι) (a : ι → ℤ),
      (∀ i, a i ≠ 0) ∧
        ∃ (eH : H ≃+ (ι → ℤ)) (eL : L ≃+ (ι → ℤ))
          (d : (ι → ℤ) →+ (ι → ℤ))
          (_eQ : (L ⧸ H) ≃+ ∀ i, ZMod (Int.natAbs (a i))),
          (∀ x i, d x i = a 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

Smith coordinates for a finite-index lattice cover

Declarations

exists_smithDiagonal_monoidAlgebra