NYLL
Module

FiniteCyclicBarPeriodicCarryIdentity.lean

Nyll.GaloisCohomology.ProP.FiniteCyclicBarPeriodicCarryIdentity
13 declarations indexed from sourceView source ↗

Module documentation

The cyclic carry identity for the bar--periodic comparison

For a specified generator g, let S(x) be the prefix 1 + g + ... + g^(r(x)-1), where r(x) is the standard representative of the generator coordinate of x. The degree-two bar differential applied to these prefixes is the carry times the full cyclic norm vector. In particular, the comparison has positive sign.

Imports2
Imported by2

Declarations

def

finiteCyclicPrefixNat

L31 ↗
ClassFieldTower.Cohomology.finiteCyclicPrefixNat
Documentation

The prefix 1 + g + ... + g^(m-1) in the left regular representation.

Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · statement
def finiteCyclicPrefixNat (g : G) (m : ℕ) : MonoidAlgebra R G
def

finiteCyclicGeneratorPrefix

L35 ↗
ClassFieldTower.Cohomology.finiteCyclicGeneratorPrefix
Documentation

The prefix whose length is the standard generator coordinate of x.

Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · statement
def finiteCyclicGeneratorPrefix
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) (x : G) : MonoidAlgebra R G
theorem

finiteCyclicGeneratorPrefix_one

L41 ↗
ClassFieldTower.Cohomology.finiteCyclicGeneratorPrefix_one
Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · statement
theorem finiteCyclicGeneratorPrefix_one
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    finiteCyclicGeneratorPrefix (R := R) g hg 1 = 0
theorem

finiteCyclicPrefixNat_zero

L48 ↗
ClassFieldTower.Cohomology.finiteCyclicPrefixNat_zero
Source context 6 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
omit [Fintype G] in
Lean source · statement
theorem finiteCyclicPrefixNat_zero (g : G) :
    finiteCyclicPrefixNat (R := R) g 0 = 0
theorem

finiteCyclicPrefixNat_succ

L53 ↗
ClassFieldTower.Cohomology.finiteCyclicPrefixNat_succ
Source context 6 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
omit [Fintype G] in
Lean source · statement
theorem finiteCyclicPrefixNat_succ (g : G) (m : ℕ) :
    finiteCyclicPrefixNat (R := R) g (m + 1) =
      finiteCyclicPrefixNat (R := R) g m + MonoidAlgebra.single (g ^ m) 1
theorem

leftRegular_single_one

L59 ↗
ClassFieldTower.Cohomology.leftRegular_single_one
Source context 6 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
omit [Fintype G] in
Lean source · statement
theorem leftRegular_single_one (x y : G) :
    (Rep.leftRegular R G).ρ x (MonoidAlgebra.single y 1) =
      MonoidAlgebra.single (x * y) 1
theorem

leftRegular_pow_single_one

L65 ↗
ClassFieldTower.Cohomology.leftRegular_pow_single_one
Source context 6 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
omit [Fintype G] in
Lean source · statement
theorem leftRegular_pow_single_one (g : G) (i j : ℕ) :
    (Rep.leftRegular R G).ρ (g ^ i) (MonoidAlgebra.single (g ^ j) 1) =
      MonoidAlgebra.single (g ^ (i + j)) 1
theorem

finiteCyclicPrefixNat_add

L72 ↗
ClassFieldTower.Cohomology.finiteCyclicPrefixNat_add
Documentation

Concatenating two prefixes translates the second one by the first power.

Source context 6 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
omit [Fintype G] in
Lean source · statement
theorem finiteCyclicPrefixNat_add (g : G) (i j : ℕ) :
    finiteCyclicPrefixNat (R := R) g i +
        (Rep.leftRegular R G).ρ (g ^ i) (finiteCyclicPrefixNat (R := R) g j) =
      finiteCyclicPrefixNat (R := R) g (i + j)
theorem

generator_pow_natCard

L96 ↗
ClassFieldTower.Cohomology.generator_pow_natCard
Source context 6 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
omit [Fintype G] in
Lean source · statement
theorem generator_pow_natCard (g : G) : g ^ Nat.card G = 1
theorem

finiteCyclicPrefixNat_card_add

L100 ↗
ClassFieldTower.Cohomology.finiteCyclicPrefixNat_card_add
Source context 6 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
omit [Fintype G] in
Lean source · statement
theorem finiteCyclicPrefixNat_card_add (g : G) (m : ℕ) :
    finiteCyclicPrefixNat (R := R) g (Nat.card G + m) =
      finiteCyclicPrefixNat (R := R) g (Nat.card G) +
        finiteCyclicPrefixNat (R := R) g m
theorem

leftRegular_prefix_sub

L109 ↗
ClassFieldTower.Cohomology.leftRegular_prefix_sub
Source context 6 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
omit [Fintype G] in
Lean source · statement
theorem leftRegular_prefix_sub (g : G) (m : ℕ) :
    (Rep.leftRegular R G).ρ g
          (finiteCyclicPrefixNat (R := R) g m) -
        finiteCyclicPrefixNat (R := R) g m =
      MonoidAlgebra.single (g ^ m) 1 - MonoidAlgebra.single 1 1
theorem

finiteCyclicGeneratorPrefix_sub

L137 ↗
ClassFieldTower.Cohomology.finiteCyclicGeneratorPrefix_sub
Documentation

The degree-one prefix has differential [x] - [1].

Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · statement
theorem finiteCyclicGeneratorPrefix_sub
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) (x : G) :
    (Rep.leftRegular R G).ρ g
          (finiteCyclicGeneratorPrefix (R := R) g hg x) -
        finiteCyclicGeneratorPrefix (R := R) g hg x =
      MonoidAlgebra.single x 1 - MonoidAlgebra.single 1 1
theorem

finiteCyclicGeneratorPrefix_carry

L148 ↗
ClassFieldTower.Cohomology.finiteCyclicGeneratorPrefix_carry
Documentation

The degree-two bar--periodic comparison identity. A carry contributes the full cyclic norm vector with positive sign.

Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · statement
theorem finiteCyclicGeneratorPrefix_carry
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) (x y : G) :
    (Rep.leftRegular R G).ρ x
          (finiteCyclicGeneratorPrefix (R := R) g hg y) -
        finiteCyclicGeneratorPrefix (R := R) g hg (x * y) +
          finiteCyclicGeneratorPrefix (R := R) g hg x =
      finiteCyclicCarry g hg x y •
        finiteCyclicPrefixNat (R := R) g (Nat.card G)

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