Documentation

TauCeti.Algebra.Homology.DG.Twisted.Cocycle

Twisting cocycles over a differential graded algebra #

A twisting cocycle on a finite set P of generators graded by ind : P β†’ β„€, with values in a differential graded algebra (π’œ, d), is a matrix m : P β†’ P β†’ A of homogeneous elements which satisfies the twisting equation

d (m x y) = Ξ£_z (-1) ^ (ind x - ind z) β€’ (m x z * m z y)

and the one-sidedness condition m x y = 0 whenever ind x ≀ ind y. It is the Barraud–Cornea structure that the compactified trajectory spaces of a Morse or Floer theory produce, by evaluating their fundamental chains into chains on a loop space, and it is the only input of the twisted complex 𝓕 βŠ— ⟨P⟩ of TauCeti.Algebra.Homology.DG.Twisted.Complex.

The source works with homological gradings, where m x y has degree ind x - ind y - 1. Tau Ceti's differential graded algebras are cohomologically graded, and the bridge C^{-n} = C_n puts m x y in cohomological degree ind y - ind x + 1. The twisting equation itself carries no grading and is stated verbatim.

The one-sidedness condition is part of the data. It does not follow from the degree and the twisting equation over an arbitrary differential graded algebra: over β„š[Ξ΅]/(Ρ²) with Ξ΅ in cohomological degree 1 and d = 0, one generator x with m x x = Ξ΅ satisfies both. It is automatic over a cohomologically nonpositive algebra, since then the degree ind y - ind x + 1 is positive when ind x ≀ ind y (TauCeti.TwistingCocycle.one_sided_of_nonpos). The cubical chains on a loop space are cohomologically nonpositive, so for every geometric cocycle the condition is a lemma.

Main definitions #

Main results #

References #

source
structure TauCeti.TwistingCocycle {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (π’œ : β„€ β†’ Submodule R A) (d : A β†’β‚—[R] A) (P : Type uP) [Fintype P] (ind : P β†’ β„€) :
Type (max uA uP)

A twisting cocycle with values in the differential graded algebra (π’œ, d), on the finite set P of generators graded by ind. The entry m x y is the coefficient of y in the twisted differential of x. It is homogeneous of cohomological degree ind y - ind x + 1, the matrix satisfies the twisting equation d (m x y) = Ξ£_z (-1) ^ (ind x - ind z) β€’ (m x z * m z y), and it is strictly upper triangular for the order by ind: m x y = 0 whenever ind x ≀ ind y.

  • m : P β†’ P β†’ A

    The coefficient of y in the twisted differential of x.

  • mem_graded (x y : P) : self.m x y ∈ π’œ (ind y - ind x + 1)

    Each entry is homogeneous, of cohomological degree ind y - ind x + 1.

  • twisting (x y : P) : d (self.m x y) = βˆ‘ z : P, (ind x - ind z).negOnePow β€’ (self.m x z * self.m z y)

    The twisting equation, in the source's homological sign convention.

  • one_sided (x y : P) : ind x ≀ ind y β†’ self.m x y = 0

    One-sidedness: the matrix is strictly upper triangular for the order by ind.

Instances For
    source
    theorem TauCeti.TwistingCocycle.one_sided_of_nonpos {R : Type uR} {A : Type uA} [Semiring R] [AddCommMonoid A] [Module R A] {π’œ : β„€ β†’ Submodule R A} {P : Type uP} {ind : P β†’ β„€} (m : P β†’ P β†’ A) (hm : βˆ€ (x y : P), m x y ∈ π’œ (ind y - ind x + 1)) (hπ’œ : βˆ€ (n : β„€), 0 < n β†’ π’œ n = βŠ₯) (x y : P) :
    ind x ≀ ind y β†’ m x y = 0

    Over a cohomologically nonpositive algebra, the degree condition alone forces one-sidedness: an entry m x y with ind x ≀ ind y lives in a positive degree, where the algebra vanishes. This is the situation of the cubical chains on a loop space. No differential and no twisting equation is involved.

    source
    theorem TauCeti.TwistingCocycle.ext {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} {d : A β†’β‚—[R] A} {P : Type uP} [Fintype P] {ind : P β†’ β„€} {m₁ mβ‚‚ : TwistingCocycle π’œ d P ind} (h : βˆ€ (x y : P), m₁.m x y = mβ‚‚.m x y) :
    m₁ = mβ‚‚
    source
    theorem TauCeti.TwistingCocycle.ext_iff {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} {d : A β†’β‚—[R] A} {P : Type uP} [Fintype P] {ind : P β†’ β„€} {m₁ mβ‚‚ : TwistingCocycle π’œ d P ind} :
    m₁ = mβ‚‚ ↔ βˆ€ (x y : P), m₁.m x y = mβ‚‚.m x y
    source
    @[simp]
    theorem TauCeti.TwistingCocycle.m_self {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} {d : A β†’β‚—[R] A} {P : Type uP} [Fintype P] {ind : P β†’ β„€} (m : TwistingCocycle π’œ d P ind) (x : P) :
    m.m x x = 0

    The diagonal of a twisting cocycle vanishes.

    source
    theorem TauCeti.TwistingCocycle.m_eq_zero_of_le {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} {d : A β†’β‚—[R] A} {P : Type uP} [Fintype P] {ind : P β†’ β„€} (m : TwistingCocycle π’œ d P ind) {x y : P} (hxy : ind x ≀ ind y) :
    m.m x y = 0

    Entries below or on the diagonal vanish.

    source
    theorem TauCeti.TwistingCocycle.m_mem_zero_of_eq_add_one {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} {d : A β†’β‚—[R] A} {P : Type uP} [Fintype P] {ind : P β†’ β„€} (m : TwistingCocycle π’œ d P ind) {x y : P} (hxy : ind x = ind y + 1) :
    m.m x y ∈ π’œ 0

    The entries between generators whose indices differ by one have degree zero.

    source
    theorem TauCeti.TwistingCocycle.m_mem_neg_one_of_eq_add_two {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} {d : A β†’β‚—[R] A} {P : Type uP} [Fintype P] {ind : P β†’ β„€} (m : TwistingCocycle π’œ d P ind) {x y : P} (hxy : ind x = ind y + 2) :
    m.m x y ∈ π’œ (-1)

    The entries between generators whose indices differ by two have degree -1.

    source
    theorem TauCeti.TwistingCocycle.m_mul_m_eq_zero_of_not_lt_lt {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} {d : A β†’β‚—[R] A} {P : Type uP} [Fintype P] {ind : P β†’ β„€} (m : TwistingCocycle π’œ d P ind) {x y z : P} (h : Β¬(ind z < ind y ∧ ind y < ind x)) :
    m.m x y * m.m y z = 0

    A product of two consecutive entries vanishes unless the middle generator has strictly intermediate index, by one-sidedness.

    source
    theorem TauCeti.TwistingCocycle.d_m_eq_zero_of_eq_add_one {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} {d : A β†’β‚—[R] A} {P : Type uP} [Fintype P] {ind : P β†’ β„€} (m : TwistingCocycle π’œ d P ind) {x y : P} (hxy : ind x = ind y + 1) :
    d (m.m x y) = 0

    The entries between generators whose indices differ by one are cycles: no generator has an index strictly between theirs.

    source
    theorem TauCeti.TwistingCocycle.sum_m_mul_m_of_eq_add_two {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} {d : A β†’β‚—[R] A} {P : Type uP} [Fintype P] {ind : P β†’ β„€} (m : TwistingCocycle π’œ d P ind) {x z : P} (hxz : ind x = ind z + 2) :
    βˆ‘ y : P, m.m x y * m.m y z = -d (m.m x z)

    The twisting equation at index difference two: between generators whose indices differ by two, the sum of the products of the entries through the generators of the intermediate index is minus the differential of the entry.

    source
    theorem TauCeti.TwistingCocycle.sum_subtype_m_mul_m_of_eq_add_two {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} {d : A β†’β‚—[R] A} {P : Type uP} [Fintype P] {ind : P β†’ β„€} (m : TwistingCocycle π’œ d P ind) {x z : P} (q : β„€) (hx : ind x = q + 1 + 1) (hz : ind z = q) :
    βˆ‘ y : { y : P // ind y = q + 1 }, m.m x ↑y * m.m (↑y) z = -d (m.m x z)

    The twisting equation at index difference two, as a sum over the generators of the intermediate index only.

    source
    @[instance_reducible]
    instance TauCeti.TwistingCocycle.instZero {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} {d : A β†’β‚—[R] A} {P : Type uP} [Fintype P] {ind : P β†’ β„€} :
    Zero (TwistingCocycle π’œ d P ind)

    The zero matrix is a twisting cocycle: both sides of the twisting equation vanish.

    source
    @[simp]
    theorem TauCeti.TwistingCocycle.zero_m {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} {d : A β†’β‚—[R] A} {P : Type uP} [Fintype P] {ind : P β†’ β„€} (x y : P) :
    m 0 x y = 0
    source
    def TauCeti.TwistingCocycle.ofNonpos {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} {d : A β†’β‚—[R] A} {P : Type uP} [Fintype P] {ind : P β†’ β„€} (m : P β†’ P β†’ A) (hm : βˆ€ (x y : P), m x y ∈ π’œ (ind y - ind x + 1)) (ht : βˆ€ (x y : P), d (m x y) = βˆ‘ z : P, (ind x - ind z).negOnePow β€’ (m x z * m z y)) (hπ’œ : βˆ€ (n : β„€), 0 < n β†’ π’œ n = βŠ₯) :
    TwistingCocycle π’œ d P ind

    A twisting cocycle over a cohomologically nonpositive algebra, from the graded matrix and the twisting equation alone: one-sidedness is supplied by one_sided_of_nonpos.

    Instances For
      source
      @[simp]
      theorem TauCeti.TwistingCocycle.ofNonpos_m {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} {d : A β†’β‚—[R] A} {P : Type uP} [Fintype P] {ind : P β†’ β„€} (m : P β†’ P β†’ A) (hm : βˆ€ (x y : P), m x y ∈ π’œ (ind y - ind x + 1)) (ht : βˆ€ (x y : P), d (m x y) = βˆ‘ z : P, (ind x - ind z).negOnePow β€’ (m x z * m z y)) (hπ’œ : βˆ€ (n : β„€), 0 < n β†’ π’œ n = βŠ₯) :
      (ofNonpos m hm ht hπ’œ).m = m