Module

Cover.lean

Nyll.EtaleFundamentalGroups.Kummer.Lattices.Cover

1 declaration indexed from sourceView source ↗

Module documentation

The lattice-algebra cover and its quotient grading

For an additive subgroup H of a lattice L, the induced map of additive monoid algebras identifies R[H] with the degree-zero subalgebra of R[L] for the quotient grading by L ⧸ H.

Imports2

Mathlib.Algebra.MonoidAlgebra.Grading
Mathlib.GroupTheory.QuotientGroup.Defs

Imported by3

theorem

range_mapDomainAlgHom_eq_gradeZero_quotient

L26 ↗

EtaleFundamentalGroups.Kummer.range_mapDomainAlgHom_eq_gradeZero_quotient

Documentation

The image of the lattice-algebra map R[H] → R[L] is exactly the degree-zero subalgebra for the canonical quotient grading by L ⧸ H.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v

Lean source · statement

theorem range_mapDomainAlgHom_eq_gradeZero_quotient
    {R : Type u} {L : Type v} [CommSemiring R] [AddCommGroup L]
    (H : AddSubgroup L) :
    (AddMonoidAlgebra.mapDomainAlgHom R R H.subtype).range =
      SetLike.GradeZero.subalgebra
        (AddMonoidAlgebra.gradeBy R (QuotientAddGroup.mk' H))

Module documentation

The lattice-algebra cover and its quotient grading

Declarations

range_mapDomainAlgHom_eq_gradeZero_quotient