NYLL
Module

FiniteCyclicBarPeriodicChainComparison.lean

Nyll.GaloisCohomology.ProP.FiniteCyclicBarPeriodicChainComparison
21 declarations indexed from sourceView source ↗

Module documentation

Low-degree bar--periodic chain comparison for finite cyclic groups

The generator prefixes and carry identity define the first four components of a map from the bar resolution to the cyclic periodic resolution. This file verifies the chain squares through degree three and extends those components to a full chain map.

Imports14
  • Nyll.GaloisCohomology.ProP.FiniteCyclicBarPeriodicCarryIdentity
  • Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
  • Mathlib.RepresentationTheory.Equiv
  • Mathlib.Algebra.BigOperators.Fin
  • Mathlib.Algebra.Group.Action.Defs
  • Mathlib.Algebra.Group.Basic
  • Mathlib.Algebra.Group.Hom.Defs
  • Mathlib.Algebra.Group.Monoid
  • Mathlib.Algebra.Module.Defs
  • Mathlib.Algebra.MonoidAlgebra.Defs
  • Mathlib.Algebra.Ring.Defs
  • Mathlib.Algebra.Ring.Commute
  • Mathlib.RepresentationTheory.Basic
  • Mathlib.RepresentationTheory.Rep.Basic
Imported by2

Declarations

def

finiteCyclicGeneratorPowEquiv

L42 ↗
ClassFieldTower.Cohomology.finiteCyclicGeneratorPowEquiv
Documentation

Powers of a specified cyclic generator enumerate the group.

Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · full declaration
def finiteCyclicGeneratorPowEquiv
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) : Fin (Nat.card G) ≃ G where
  toFun i := g ^ i.val
  invFun x := ⟨(finiteCyclicGeneratorCoordinate g hg x).val, ZMod.val_lt _⟩
  left_inv i := by
    apply Fin.ext
    change (finiteCyclicGeneratorCoordinate g hg (g ^ i.val)).val = i.val
    rw [finiteCyclicGeneratorCoordinate_pow]
    exact ZMod.val_natCast_of_lt i.isLt
  right_inv x := finiteCyclicGenerator_zpow_coordinate g hg x
theorem

finiteCyclicPrefixNat_card_eq_norm_one

L54 ↗
ClassFieldTower.Cohomology.finiteCyclicPrefixNat_card_eq_norm_one
Documentation

The full generator prefix is the norm of the unit basis vector.

Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · statement
theorem finiteCyclicPrefixNat_card_eq_norm_one
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    finiteCyclicPrefixNat (R := R) g (Nat.card G) =
      (Rep.leftRegular R G).norm.hom (MonoidAlgebra.single 1 1)
def

finiteCyclicBarToPeriodicZero

L72 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicZero
Documentation

Degree zero of the explicit map from the bar resolution to the periodic resolution.

Source context 6 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
omit [Fintype G] in
Lean source · statement
def finiteCyclicBarToPeriodicZero :
    Rep.free R G (Fin 0 → G) ⟶ Rep.leftRegular R G
def

finiteCyclicBarToPeriodicOne

L78 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicOne
Documentation

Degree one of the explicit bar--periodic map.

Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · statement
def finiteCyclicBarToPeriodicOne
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    Rep.free R G (Fin 1 → G) ⟶ Rep.leftRegular R G
def

finiteCyclicBarToPeriodicTwo

L85 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicTwo
Documentation

Degree two of the explicit bar--periodic map is the positive carry.

Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · statement
def finiteCyclicBarToPeriodicTwo
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    Rep.free R G (Fin 2 → G) ⟶ Rep.leftRegular R G
def

finiteCyclicBarToPeriodicThree

L93 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicThree
Documentation

Degree three of the explicit bar--periodic map.

Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · statement
def finiteCyclicBarToPeriodicThree
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    Rep.free R G (Fin 3 → G) ⟶ Rep.leftRegular R G
theorem

finiteCyclicBarToPeriodicZero_generator

L102 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicZero_generator
Source context 6 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
omit [Fintype G] in
Lean source · statement
theorem finiteCyclicBarToPeriodicZero_generator (x : Fin 0 → G) :
    (finiteCyclicBarToPeriodicZero (R := R) (G := G)).hom
        (Finsupp.single x (MonoidAlgebra.single 1 1)) =
      MonoidAlgebra.single 1 1
theorem

finiteCyclicBarToPeriodicOne_generator

L109 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicOne_generator
Source context 5 commands

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

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

finiteCyclicBarToPeriodicTwo_generator

L117 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicTwo_generator
Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · statement
theorem finiteCyclicBarToPeriodicTwo_generator
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) (x : Fin 2 → G) :
    (finiteCyclicBarToPeriodicTwo (R := R) g hg).hom
        (Finsupp.single x (MonoidAlgebra.single 1 1)) =
      finiteCyclicCarry g hg (x 0) (x 1) • MonoidAlgebra.single 1 1
theorem

finiteCyclicBarToPeriodicThree_generator

L125 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicThree_generator
Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · statement
theorem finiteCyclicBarToPeriodicThree_generator
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) (x : Fin 3 → G) :
    (finiteCyclicBarToPeriodicThree (R := R) g hg).hom
        (Finsupp.single x (MonoidAlgebra.single 1 1)) =
      finiteCyclicCarry g hg (x 1) (x 2) •
        finiteCyclicGeneratorPrefix (R := R) g hg (x 0)
theorem

finiteCyclicBarToPeriodicOne_comm

L134 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicOne_comm
Documentation

The degree-one comparison square.

Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · statement
theorem finiteCyclicBarToPeriodicOne_comm
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    finiteCyclicBarToPeriodicOne (R := R) g hg ≫
        (Rep.applyAsHom (Rep.leftRegular R G) g - 𝟙 (Rep.leftRegular R G)) =
      Rep.barComplex.d R G 0 ≫ finiteCyclicBarToPeriodicZero (R := R) (G := G)
theorem

finiteCyclicBarToPeriodicTwo_comm

L151 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicTwo_comm
Documentation

The degree-two comparison square; the carry has positive sign.

Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · statement
theorem finiteCyclicBarToPeriodicTwo_comm
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    finiteCyclicBarToPeriodicTwo (R := R) g hg ≫ (Rep.leftRegular R G).norm =
      Rep.barComplex.d R G 1 ≫ finiteCyclicBarToPeriodicOne (R := R) g hg
theorem

finiteCyclicBarToPeriodicThree_comm

L166 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicThree_comm
Documentation

The degree-three comparison square follows from the carry cocycle law.

Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · statement
theorem finiteCyclicBarToPeriodicThree_comm
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    finiteCyclicBarToPeriodicThree (R := R) g hg ≫
        (Rep.applyAsHom (Rep.leftRegular R G) g - 𝟙 (Rep.leftRegular R G)) =
      Rep.barComplex.d R G 2 ≫ finiteCyclicBarToPeriodicTwo (R := R) g hg
def

finiteCyclicBarToPeriodicAux

L214 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicAux
Documentation

Inductive data extending the explicit degree-zero through degree-three components to every degree.

Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · full declaration
def finiteCyclicBarToPeriodicAux
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    ∀ n : ℕ,
      Σ' (f :
          (Rep.barResolution R G).complex.X n ⟶
            (Rep.FiniteCyclicGroup.resolution R g hg).complex.X n)
        (f' :
          (Rep.barResolution R G).complex.X (n + 1) ⟶
            (Rep.FiniteCyclicGroup.resolution R g hg).complex.X (n + 1)),
        f' ≫ (Rep.FiniteCyclicGroup.resolution R g hg).complex.d (n + 1) n =
          (Rep.barResolution R G).complex.d (n + 1) n ≫ f
  | 0 => ⟨finiteCyclicBarToPeriodicZero (R := R) (G := G),
      finiteCyclicBarToPeriodicOne (R := R) g hg,
      finiteCyclicBarToPeriodicOne_comm (R := R) g hg⟩
  | 1 => ⟨finiteCyclicBarToPeriodicOne (R := R) g hg,
      finiteCyclicBarToPeriodicTwo (R := R) g hg,
      finiteCyclicBarToPeriodicTwo_comm (R := R) g hg⟩
  | 2 => ⟨finiteCyclicBarToPeriodicTwo (R := R) g hg,
      finiteCyclicBarToPeriodicThree (R := R) g hg,
      finiteCyclicBarToPeriodicThree_comm (R := R) g hg⟩
  | n + 3 =>
      let p := finiteCyclicBarToPeriodicAux g hg (n + 2)
      let q := ProjectiveResolution.liftFSucc
        (Rep.barResolution R G)
        (Rep.FiniteCyclicGroup.resolution R g hg) (n + 2)
        p.1 p.2.1 p.2.2
      ⟨p.2.1, q.1, q.2⟩
theorem

finiteCyclicBarToPeriodicAux_succ

L242 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicAux_succ
Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · statement
theorem finiteCyclicBarToPeriodicAux_succ
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) (n : ℕ) :
    (finiteCyclicBarToPeriodicAux (R := R) g hg (n + 1)).1 =
      (finiteCyclicBarToPeriodicAux (R := R) g hg n).2.1
def

finiteCyclicBarToPeriodicComparison

L255 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicComparison
Documentation

The full bar-to-periodic chain map with the carry as its degree-two component. Only degrees at least four use an abstract projective lift.

Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · full declaration
def finiteCyclicBarToPeriodicComparison
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    Rep.barComplex R G ⟶
      (Rep.FiniteCyclicGroup.resolution R g hg).complex where
  f n := (finiteCyclicBarToPeriodicAux (R := R) g hg n).1
  comm' n m := by
    rintro (rfl : m + 1 = n)
    rw [finiteCyclicBarToPeriodicAux_succ]
    exact (finiteCyclicBarToPeriodicAux (R := R) g hg m).2.2
theorem

finiteCyclicBarToPeriodicComparison_f_zero

L266 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicComparison_f_zero
Source context 5 commands

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

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

finiteCyclicBarToPeriodicComparison_f_one

L272 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicComparison_f_one
Source context 5 commands

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

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

finiteCyclicBarToPeriodicComparison_f_two

L278 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicComparison_f_two
Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · statement
theorem finiteCyclicBarToPeriodicComparison_f_two
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    (finiteCyclicBarToPeriodicComparison (R := R) g hg).f 2 =
      finiteCyclicBarToPeriodicTwo (R := R) g hg
theorem

finiteCyclicBarToPeriodicComparison_f_three

L284 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicComparison_f_three
Source context 5 commands

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

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

finiteCyclicBarToPeriodicResolutionHom

L291 ↗
ClassFieldTower.Cohomology.finiteCyclicBarToPeriodicResolutionHom
Documentation

The explicit comparison, regarded as a morphism of projective resolutions lifting the identity of the trivial representation.

Source context 5 commands

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

namespace ClassFieldTower.Cohomology
noncomputable section
open CategoryTheory Representation
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
Lean source · full declaration
def finiteCyclicBarToPeriodicResolutionHom
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    ProjectiveResolution.Hom
      (Rep.barResolution R G)
      (Rep.FiniteCyclicGroup.resolution R g hg) (𝟙 _) where
  hom := finiteCyclicBarToPeriodicComparison (R := R) g hg
  hom_f_zero_comp_π_f_zero := by
    apply Rep.free_ext R G (Rep.trivial R G R)
    intro x
    let h : G := 1
    have H :
        (Rep.diagonalSuccIsoFree R G 0).inv.hom
            (Finsupp.single x (MonoidAlgebra.single h 1)) =
          MonoidAlgebra.single (h • Fin.partialProd x) (1 : R) := by
      simp only [Rep.diagonalSuccIsoFree, Rep.diagonalSuccIsoTensorTrivial,
        Iso.trans_inv, Rep.hom_comp,
        Representation.IntertwiningMap.comp_apply]
      have step1 :
          (Rep.Hom.hom
              (Rep.leftRegularTensorTrivialIsoFree R G (Fin 0 → G)).inv)
              (Finsupp.single x (MonoidAlgebra.single h 1)) =
            MonoidAlgebra.single h 1 ⊗ₜ[R] MonoidAlgebra.single x 1 :=
        Representation.leftRegularTensorTrivialIsoFree_symm_apply_single_single
          x h 1
      rw [step1]
      have key₁ := Representation.linearizeMap_single (k := R)
        (Action.diagonalSuccIsoTensorTrivial G 0).inv (h, x)
          ((1 : R) * 1)
      have key₂ :=
        Representation.LinearizeMonoidal.μ_apply_single_single (k := R)
          (X := Action.leftRegular G)
          (Y := Action.trivial G (Fin 0 → G)) h x 1 1
      exact ((congrArg (fun z ↦
        Representation.linearizeMap
          (Action.diagonalSuccIsoTensorTrivial G 0).inv z) key₂).trans
            key₁).trans (by
              congr 1
              · exact Action.diagonalSuccIsoTensorTrivial_inv_hom_apply h x
              · simp)
    change
      ((Rep.trivial R G R).leftRegularHom 1).hom
          ((finiteCyclicBarToPeriodicZero (R := R) (G := G)).hom
            (Finsupp.single x (MonoidAlgebra.single 1 1))) =
        (Rep.standardComplex.ε R G).hom
          ((Rep.diagonalSuccIsoFree R G 0).inv.hom
            (Finsupp.single x (MonoidAlgebra.single 1 1)))
    rw [finiteCyclicBarToPeriodicZero_generator]
    rw [show (1 : G) = h by simp [h], H]
    simp [Rep.standardComplex.ε, h]

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