Module

CharacterAction.lean

Nyll.EtaleFundamentalGroups.Kummer.Lattices.CharacterAction

10 declarations indexed from sourceView source ↗

Module documentation

Character action on a finite-index lattice cover

Characters of the finite quotient lattice act diagonally on the ambient lattice algebra. When the coefficient domain has enough roots of unity, these characters separate the quotient degrees. Consequently their common fixed subalgebra is exactly the image of the subgroup lattice algebra.

Imports2

Mathlib.GroupTheory.FiniteAbelian.Duality
Nyll.EtaleFundamentalGroups.Kummer.Lattices.Cover

Imported by2

def

latticeCharacterWeight

L25 ↗

EtaleFundamentalGroups.Kummer.latticeCharacterWeight

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v
noncomputable section

Lean source · statement

def latticeCharacterWeight
    {k : Type u} {L : Type v} [CommRing k] [AddCommGroup L]
    (H : AddSubgroup L) (χ : Multiplicative (L ⧸ H) →* kˣ) :
    Multiplicative L →* k

def

latticeCharacterMonomial

L32 ↗

EtaleFundamentalGroups.Kummer.latticeCharacterMonomial

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v
noncomputable section

Lean source · statement

def latticeCharacterMonomial
    {k : Type u} {L : Type v} [CommRing k] [AddCommGroup L]
    (H : AddSubgroup L) (χ : Multiplicative (L ⧸ H) →* kˣ) :
    Multiplicative L →* AddMonoidAlgebra k L

def

latticeCharacterAlgHom

L41 ↗

EtaleFundamentalGroups.Kummer.latticeCharacterAlgHom

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v
noncomputable section

Lean source · statement

def latticeCharacterAlgHom
    {k : Type u} {L : Type v} [CommRing k] [AddCommGroup L]
    (H : AddSubgroup L) (χ : Multiplicative (L ⧸ H) →* kˣ) :
    AddMonoidAlgebra k L →ₐ[k] AddMonoidAlgebra k L

theorem

latticeCharacterAlgHom_single

L49 ↗

EtaleFundamentalGroups.Kummer.latticeCharacterAlgHom_single

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v
noncomputable section

Lean source · statement

theorem latticeCharacterAlgHom_single
    {k : Type u} {L : Type v} [CommRing k] [AddCommGroup L]
    (H : AddSubgroup L) (χ : Multiplicative (L ⧸ H) →* kˣ)
    (l : L) (a : k) :
    latticeCharacterAlgHom H χ (AddMonoidAlgebra.single l a) =
      AddMonoidAlgebra.single l
        (a * (χ (Multiplicative.ofAdd (QuotientAddGroup.mk' H l)) : k))

def

latticeCharacterAlgEquiv

L59 ↗

EtaleFundamentalGroups.Kummer.latticeCharacterAlgEquiv

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v
noncomputable section

Lean source · statement

def latticeCharacterAlgEquiv
    {k : Type u} {L : Type v} [CommRing k] [AddCommGroup L]
    (H : AddSubgroup L) (χ : Multiplicative (L ⧸ H) →* kˣ) :
    AddMonoidAlgebra k L ≃ₐ[k] AddMonoidAlgebra k L

def

latticeCharacterAction

L79 ↗

EtaleFundamentalGroups.Kummer.latticeCharacterAction

Documentation

The canonical diagonal action of quotient-lattice characters on the ambient lattice algebra.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v
noncomputable section

Lean source · full declaration

def latticeCharacterAction
    {k : Type u} {L : Type v} [CommRing k] [AddCommGroup L]
    (H : AddSubgroup L) :
    (Multiplicative (L ⧸ H) →* kˣ) →*
      (AddMonoidAlgebra k L ≃ₐ[k] AddMonoidAlgebra k L) where
  toFun := latticeCharacterAlgEquiv H
  map_one' := by
    apply AlgEquiv.coe_toAlgHom_injective
    apply AddMonoidAlgebra.algHom_ext
    · intro l
      simp [latticeCharacterAlgEquiv, latticeCharacterAlgHom_single]
    · ext
  map_mul' χ ψ := by
    apply AlgEquiv.coe_toAlgHom_injective
    apply AddMonoidAlgebra.algHom_ext
    · intro l
      simp [latticeCharacterAlgEquiv, latticeCharacterAlgHom_single,
        AlgEquiv.mul_apply, mul_comm]
    · ext

theorem

latticeCharacterAction_single

L100 ↗

EtaleFundamentalGroups.Kummer.latticeCharacterAction_single

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v
noncomputable section

Lean source · statement

theorem latticeCharacterAction_single
    {k : Type u} {L : Type v} [CommRing k] [AddCommGroup L]
    (H : AddSubgroup L) (χ : Multiplicative (L ⧸ H) →* kˣ)
    (l : L) (a : k) :
    latticeCharacterAction H χ (AddMonoidAlgebra.single l a) =
      AddMonoidAlgebra.single l
        (a * (χ (Multiplicative.ofAdd (QuotientAddGroup.mk' H l)) : k))

theorem

latticeCharacterAction_coeff

L109 ↗

EtaleFundamentalGroups.Kummer.latticeCharacterAction_coeff

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v
noncomputable section

Lean source · statement

theorem latticeCharacterAction_coeff
    {k : Type u} {L : Type v} [CommRing k] [AddCommGroup L]
    (H : AddSubgroup L) (χ : Multiplicative (L ⧸ H) →* kˣ)
    (x : AddMonoidAlgebra k L) (l : L) :
    (latticeCharacterAction H χ x).coeff l =
      x.coeff l * (χ (Multiplicative.ofAdd (QuotientAddGroup.mk' H l)) : k)

theorem

fixedBy_latticeCharacterAction_eq_gradeZero

L141 ↗

EtaleFundamentalGroups.Kummer.fixedBy_latticeCharacterAction_eq_gradeZero

Documentation

The elements fixed by every quotient character are exactly the degree-zero part for the quotient grading.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v
noncomputable section

Lean source · statement

theorem fixedBy_latticeCharacterAction_eq_gradeZero
    {k : Type u} {L : Type v} [CommRing k] [IsDomain k]
    [AddCommGroup L]
    (H : AddSubgroup L) [Finite (L ⧸ H)]
    [HasEnoughRootsOfUnity k
      (Monoid.exponent (Multiplicative (L ⧸ H)))] :
    {x : AddMonoidAlgebra k L |
        ∀ χ : Multiplicative (L ⧸ H) →* kˣ,
          latticeCharacterAction H χ x = x} =
      (SetLike.GradeZero.subalgebra
        (AddMonoidAlgebra.gradeBy k (QuotientAddGroup.mk' H)) :
        Set (AddMonoidAlgebra k L))

theorem

fixedBy_latticeCharacterAction_eq_range

L188 ↗

EtaleFundamentalGroups.Kummer.fixedBy_latticeCharacterAction_eq_range

Documentation

The common fixed subalgebra of quotient characters is the image of the subgroup lattice algebra.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v
noncomputable section

Lean source · statement

theorem fixedBy_latticeCharacterAction_eq_range
    {k : Type u} {L : Type v} [CommRing k] [IsDomain k]
    [AddCommGroup L]
    (H : AddSubgroup L) [Finite (L ⧸ H)]
    [HasEnoughRootsOfUnity k
      (Monoid.exponent (Multiplicative (L ⧸ H)))] :
    {x : AddMonoidAlgebra k L |
        ∀ χ : Multiplicative (L ⧸ H) →* kˣ,
          latticeCharacterAction H χ x = x} =
      ((AddMonoidAlgebra.mapDomainAlgHom k k H.subtype).range :
        Set (AddMonoidAlgebra k L))

Module documentation

Character action on a finite-index lattice cover

Declarations