NYLL
Module

FiniteLinearization.lean

Nyll.ProCGroups.ProP.Zassenhaus.FiniteLinearization
7 declarations indexed from sourceView source ↗

Module documentation

First-order characters of an ordinary group algebra

An additive ZMod p character defines a group-algebra map into the dual numbers. Its square-zero coordinate detects degree one, so the square of the augmentation ideal is annihilated. This is the separation mechanism used in the reverse degree-two Zassenhaus inclusion.

Imports2
Imported by2

Declarations

def

characterLinearizationMonoidHom

L31 ↗
ClassFieldTower.ProP.characterLinearizationMonoidHom
Documentation

An additive character as the square-zero coordinate of a multiplicative unit.

Source context 6 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
Lean source · full declaration
def characterLinearizationMonoidHom (χ : Additive Q →+ ZMod p) :
    Q →* TrivSqZeroExt (ZMod p) (ZMod p) where
  toFun q :=
    TrivSqZeroExt.inl (M := ZMod p) 1 +
      TrivSqZeroExt.inr (R := ZMod p) (χ (Additive.ofMul q))
  map_one' := by
    apply TrivSqZeroExt.ext <;> simp
  map_mul' := by
    intro a b
    apply TrivSqZeroExt.ext
    · simp
    · simp [add_comm]
def

characterLinearization

L45 ↗
ClassFieldTower.ProP.characterLinearization
Documentation

The group-algebra map recording augmentation and a character to first order.

Source context 6 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
Lean source · statement
def characterLinearization (χ : Additive Q →+ ZMod p) :
    MonoidAlgebra (ZMod p) Q →ₐ[ZMod p]
      TrivSqZeroExt (ZMod p) (ZMod p)
theorem

characterLinearization_fst

L53 ↗
ClassFieldTower.ProP.characterLinearization_fst
Documentation

The first coordinate of character linearization is augmentation.

Source context 6 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
Lean source · statement
theorem characterLinearization_fst (χ : Additive Q →+ ZMod p)
    (x : MonoidAlgebra (ZMod p) Q) :
    (characterLinearization p Q χ x).fst =
      groupAlgebraAugmentation (ZMod p) Q x
theorem

characterLinearization_eq_inr_of_mem_augmentationIdeal

L80 ↗
ClassFieldTower.ProP.characterLinearization_eq_inr_of_mem_augmentationIdeal
Documentation

On the augmentation ideal, character linearization has only its square-zero coordinate.

Source context 6 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
Lean source · statement
theorem characterLinearization_eq_inr_of_mem_augmentationIdeal
    (χ : Additive Q →+ ZMod p) {x : MonoidAlgebra (ZMod p) Q}
    (hx : x ∈ groupAlgebraAugmentationIdeal (ZMod p) Q) :
    characterLinearization p Q χ x =
      TrivSqZeroExt.inr (characterLinearization p Q χ x).snd
theorem

characterLinearization_mul_eq_zero_of_mem_augmentationIdeal

L92 ↗
ClassFieldTower.ProP.characterLinearization_mul_eq_zero_of_mem_augmentationIdeal
Documentation

The product of two augmentation-ideal elements is killed by character linearization.

Source context 6 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
Lean source · statement
theorem characterLinearization_mul_eq_zero_of_mem_augmentationIdeal
    (χ : Additive Q →+ ZMod p) {x y : MonoidAlgebra (ZMod p) Q}
    (hx : x ∈ groupAlgebraAugmentationIdeal (ZMod p) Q)
    (hy : y ∈ groupAlgebraAugmentationIdeal (ZMod p) Q) :
    characterLinearization p Q χ (x * y) = 0
theorem

characterLinearization_eq_zero_of_mem_augmentationIdeal_sq

L103 ↗
ClassFieldTower.ProP.characterLinearization_eq_zero_of_mem_augmentationIdeal_sq
Documentation

Character linearization annihilates the square of the augmentation ideal.

Source context 6 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
Lean source · statement
theorem characterLinearization_eq_zero_of_mem_augmentationIdeal_sq
    (χ : Additive Q →+ ZMod p) {x : MonoidAlgebra (ZMod p) Q}
    (hx : x ∈ (groupAlgebraAugmentationIdeal (ZMod p) Q) ^ 2) :
    characterLinearization p Q χ x = 0
theorem

character_eq_zero_of_generator_mem_augmentationIdeal_sq

L123 ↗
ClassFieldTower.ProP.character_eq_zero_of_generator_mem_augmentationIdeal_sq
Documentation

If [q]-1 lies in the augmentation square, every additive character vanishes on q.

Source context 6 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
Lean source · statement
theorem character_eq_zero_of_generator_mem_augmentationIdeal_sq
    (χ : Additive Q →+ ZMod p) (q : Q)
    (hq : groupAlgebraAugmentationGenerator (ZMod p) Q q ∈
      (groupAlgebraAugmentationIdeal (ZMod p) Q) ^ 2) :
    χ (Additive.ofMul q) = 0

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.