FiniteCyclicCarryCocycle.lean

def finiteCyclicGeneratorCoordinate
    {G : Type u} [Group G] [Fintype G]
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) (x : G) :
    ZMod (Nat.card G)

theorem finiteCyclicGeneratorCoordinate_one
    {G : Type u} [Group G] [Fintype G]
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    finiteCyclicGeneratorCoordinate g hg 1 = 0

theorem finiteCyclicGeneratorCoordinate_generator
    {G : Type u} [Group G] [Fintype G]
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    finiteCyclicGeneratorCoordinate g hg g = 1

theorem finiteCyclicGeneratorCoordinate_mul
    {G : Type u} [Group G] [Fintype G]
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) (x y : G) :
    finiteCyclicGeneratorCoordinate g hg (x * y) =
      finiteCyclicGeneratorCoordinate g hg x +
        finiteCyclicGeneratorCoordinate g hg y

theorem finiteCyclicGeneratorCoordinate_zpow
    {G : Type u} [Group G] [Fintype G]
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) (i : ℤ) :
    finiteCyclicGeneratorCoordinate g hg (g ^ i) =
      (i : ZMod (Nat.card G))

theorem finiteCyclicGeneratorCoordinate_pow
    {G : Type u} [Group G] [Fintype G]
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) (i : ℕ) :
    finiteCyclicGeneratorCoordinate g hg (g ^ i) =
      (i : ZMod (Nat.card G))

theorem finiteCyclicGeneratorCoordinate_injective
    {G : Type u} [Group G] [Fintype G]
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    Function.Injective (finiteCyclicGeneratorCoordinate g hg)

theorem finiteCyclicGenerator_zpow_coordinate
    {G : Type u} [Group G] [Fintype G]
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) (x : G) :
    g ^ (finiteCyclicGeneratorCoordinate g hg x).val = x

def zmodCarry {n : ℕ} [NeZero n] (x y : ZMod n) : ℕ

theorem zmodCarry_eq_one_iff {n : ℕ} [NeZero n] (x y : ZMod n) :
    zmodCarry x y = 1 ↔ n ≤ x.val + y.val

theorem zmodCarry_eq_zero_iff {n : ℕ} [NeZero n] (x y : ZMod n) :
    zmodCarry x y = 0 ↔ x.val + y.val < n

theorem zmodCarry_zero_left {n : ℕ} [NeZero n] (x : ZMod n) :
    zmodCarry 0 x = 0

theorem zmodCarry_zero_right {n : ℕ} [NeZero n] (x : ZMod n) :
    zmodCarry x 0 = 0

theorem zmodCarry_cocycle {n : ℕ} [NeZero n] (x y z : ZMod n) :
    zmodCarry (x + y) z + zmodCarry x y =
      zmodCarry y z + zmodCarry x (y + z)

def finiteCyclicCarry
    {G : Type u} [Group G] [Fintype G]
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) (x y : G) : ℕ

theorem finiteCyclicCarry_one_left
    {G : Type u} [Group G] [Fintype G]
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) (x : G) :
    finiteCyclicCarry g hg 1 x = 0

theorem finiteCyclicCarry_one_right
    {G : Type u} [Group G] [Fintype G]
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) (x : G) :
    finiteCyclicCarry g hg x 1 = 0

theorem finiteCyclicCarry_cocycle
    {G : Type u} [Group G] [Fintype G]
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g) (x y z : G) :
    finiteCyclicCarry g hg (x * y) z + finiteCyclicCarry g hg x y =
      finiteCyclicCarry g hg y z + finiteCyclicCarry g hg x (y * z)

theorem finiteCyclicCarry_zpow_val
    {G : Type u} [Group G] [Fintype G]
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (i j : ZMod (Nat.card G)) :
    finiteCyclicCarry g hg (g ^ i.val) (g ^ j.val) = zmodCarry i j

def finiteCyclicCarryTwoCocycle
    {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
    (A : Rep R G) (g : G)
    (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap) :
    groupCohomology.cocycles₂ A

theorem finiteCyclicCarryTwoCocycle_apply
    {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
    (A : Rep R G) (g : G)
    (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap)
    (x y : G) :
    finiteCyclicCarryTwoCocycle A g hg a (x, y) =
      finiteCyclicCarry g hg x y • a.1

theorem finiteCyclicCarryTwoCocycle_zpow_val
    {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
    (A : Rep R G) (g : G)
    (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap)
    (i j : ZMod (Nat.card G)) :
    finiteCyclicCarryTwoCocycle A g hg a (g ^ i.val, g ^ j.val) =
      zmodCarry i j • a.1

theorem finiteCyclicCarryTwoCocycle_one_left
    {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
    (A : Rep R G) (g : G)
    (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap)
    (x : G) :
    finiteCyclicCarryTwoCocycle A g hg a (1, x) = 0

theorem finiteCyclicCarryTwoCocycle_one_right
    {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
    (A : Rep R G) (g : G)
    (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap)
    (x : G) :
    finiteCyclicCarryTwoCocycle A g hg a (x, 1) = 0