Lemma 10.2 as stated: normalized, and in every weight

lem:mod-four-comparison (integral-deformations.tex): "Let μ̄ be a normalized Hochschild two-cocycle of A⁽²⁾ of internal degree q > 0. Then 2μ̃ is a coboundary in the normalized Hochschild complex of A⁽⁴⁾. The assertion holds separately in every simultaneous integer weight."

2μ̃ is any μO with μO(a, b) = 2x whenever x lifts μ̄(πa, πb); it is a cocycle (isHCocycle_twice) and normalized (twice_one_left, twice_one_right). The coboundary of exists_hcobdry_twice is then normalized, h(1) = 0 (exists_normalized_cobdry). For ray weights hv : R → M lifting a mesh weight W (the rays Θ(b_r) homogeneous of weight hv r), the weight projections wProjO m of 𝒪P shift along products of ray vectors (wProjO_mul_left, wProjO_mul_right); if μ̄ has character χ, so has 2μ̃ (twice_char), and the weight-χ part of the coboundary is again a normalized coboundary of 2μ̃ (exists_normalized_cobdry_weight).

theorem MultiplicativeBasisDeformations.MGr.repr_eq_zero {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [DecidableEq M] {N : Type u_3} [AddCommGroup N] [Module K N] (G : MGr K M N) {ι : Type u_4} [Fintype ι] (β : Module.Basis ι K N) (w : ι → M) (hβ : ∀ (i : ι), G.IsHom (w i) (β i)) {m : M} {n : N} (hn : G.IsHom m n) {i : ι} (hi : w i ≠ m) : (β.repr n) i = 0

Coefficients of a homogeneous element along a homogeneous basis vanish off its weight.

noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.wProjO {V' R : Type} [Fintype V'] [DecidableEq V'] [Fintype R] [DecidableEq R] (P : Mult V' R) {M : Type} (hv : R → M) (m : M) : ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4))

The weight-m projection of 𝒪P along the ray basis.

theorem MultiplicativeBasisDeformations.RaySys.Mult.wProjO_b {V' R : Type} [Fintype V'] [DecidableEq V'] [Fintype R] [DecidableEq R] (P : Mult V' R) {M : Type} [AddCommGroup M] (hv : R → M) (m : M) (t : R) : (P.wProjO hv m) (P.b (ZMod 4) t) = if hv t = m then P.b (ZMod 4) t else 0

theorem MultiplicativeBasisDeformations.RaySys.Mult.wProjO_wProjO {V' R : Type} [Fintype V'] [DecidableEq V'] [Fintype R] [DecidableEq R] (P : Mult V' R) {M : Type} [AddCommGroup M] (hv : R → M) (m : M) (y : ↥(P.Lin (ZMod 4))) : (P.wProjO hv m) ((P.wProjO hv m) y) = (P.wProjO hv m) y

theorem MultiplicativeBasisDeformations.RaySys.Mult.wProjO_mul_left {V' R : Type} [Fintype V'] [DecidableEq V'] [Fintype R] [DecidableEq R] (P : Mult V' R) {M : Type} [AddCommGroup M] (hv : R → M) (hv_mul : ∀ (a b t : R), P.mul a b = some t → hv t = hv a + hv b) (r : R) (m : M) (y : ↥(P.Lin (ZMod 4))) : (P.wProjO hv m) (P.b (ZMod 4) r * y) = P.b (ZMod 4) r * (P.wProjO hv (m - hv r)) y

theorem MultiplicativeBasisDeformations.RaySys.Mult.wProjO_mul_right {V' R : Type} [Fintype V'] [DecidableEq V'] [Fintype R] [DecidableEq R] (P : Mult V' R) {M : Type} [AddCommGroup M] (hv : R → M) (hv_mul : ∀ (a b t : R), P.mul a b = some t → hv t = hv a + hv b) (s : R) (m : M) (y : ↥(P.Lin (ZMod 4))) : (P.wProjO hv m) (y * P.b (ZMod 4) s) = (P.wProjO hv (m - hv s)) y * P.b (ZMod 4) s

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.Coch2 {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) : Type

Two-cochains of A⁽²⁾.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.Coch2O {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {R : Type} [Fintype R] [DecidableEq R] (P : RaySys.Mult D.PV R) : Type

Two-cochains of 𝒪P.

2μ̃ is a normalized cocycle

theorem MultiplicativeBasisDeformations.MeshWalk.two_smul_eq_of_πO {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {x y : ↥(P.Lin (ZMod 4))} (h : (πO T) x = (πO T) y) : 2 • x = 2 • y

Twice an element of 𝒪P depends only on its reduction.

theorem MultiplicativeBasisDeformations.MeshWalk.isHCocycle_twice {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {μ : Coch2 D} {μO : Coch2O P} (hμO : ∀ (a b x : ↥(P.Lin (ZMod 4))), (πO T) x = (μ ((πO T) a)) ((πO T) b) → (μO a) b = 2 • x) (hμ : GExt.IsHCocycle μ) : GExt.IsHCocycle μO

2μ̃ is a cocycle.

theorem MultiplicativeBasisDeformations.MeshWalk.twice_one_left {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {μ : Coch2 D} {μO : Coch2O P} (hμO : ∀ (a b x : ↥(P.Lin (ZMod 4))), (πO T) x = (μ ((πO T) a)) ((πO T) b) → (μO a) b = 2 • x) (hn : ∀ (b : (CatAlg.Alg D.F0)ᵐᵒᵖ), (μ 1) b = 0) (b : ↥(P.Lin (ZMod 4))) : (μO 1) b = 0

theorem MultiplicativeBasisDeformations.MeshWalk.twice_one_right {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {μ : Coch2 D} {μO : Coch2O P} (hμO : ∀ (a b x : ↥(P.Lin (ZMod 4))), (πO T) x = (μ ((πO T) a)) ((πO T) b) → (μO a) b = 2 • x) (hn : ∀ (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), (μ a) 1 = 0) (a : ↥(P.Lin (ZMod 4))) : (μO a) 1 = 0

The normalized coboundary

theorem MultiplicativeBasisDeformations.MeshWalk.exists_normalized_cobdry {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {μ : Coch2 D} {μO : Coch2O P} (hμO : ∀ (a b x : ↥(P.Lin (ZMod 4))), (πO T) x = (μ ((πO T) a)) ((πO T) b) → (μO a) b = 2 • x) (J : D.InjData) (h1 : DegOne D) {S : ScalarMeshCategory.RowSet Q} (hspan : ScalarMeshCategory.CokerSpan c S) (htwo : ScalarMeshCategory.TwoRows Q S) {q : ℕ} (hq : 1 ≤ q) (hμ : GExt.IsHCocycle μ) (hdeg : GExt.HDeg (galgA0 D ⋯) μ ↑q) (hn : ∀ (b : (CatAlg.Alg D.F0)ᵐᵒᵖ), (μ 1) b = 0) : ∃ (h : ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4))), μO = GExt.hcobdry h ∧ h 1 = 0

Lemma 10.2 (lem:mod-four-comparison): for a normalized cocycle μ̄ of A⁽²⁾ of internal degree q > 0, 2μ̃ is the coboundary of a normalized one-cochain h of A⁽⁴⁾ = 𝒪P.

Weights

theorem MultiplicativeBasisDeformations.MeshWalk.twice_char {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {μ : Coch2 D} {μO : Coch2O P} (hμO : ∀ (a b x : ↥(P.Lin (ZMod 4))), (πO T) x = (μ ((πO T) a)) ((πO T) b) → (μO a) b = 2 • x) {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hv : R → M) (hΘ : ∀ (a : R), (grA0 W ⋯ D).IsHom (hv a) (T.Θ (P.b (ZMod 2) a))) {χ : M} (hχ : ∀ (α β : M) (a b : (CatAlg.Alg D.F0)ᵐᵒᵖ), (grA0 W ⋯ D).IsHom α a → (grA0 W ⋯ D).IsHom β b → (grA0 W ⋯ D).IsHom (α + β + χ) ((μ a) b)) (r s : R) : (P.wProjO hv (hv r + hv s + χ)) ((μO (P.b (ZMod 4) r)) (P.b (ZMod 4) s)) = (μO (P.b (ZMod 4) r)) (P.b (ZMod 4) s)

2μ̃ has the character of μ̄.

theorem MultiplicativeBasisDeformations.MeshWalk.cobdry_weight {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {μ : Coch2 D} {μO : Coch2O P} (hμO : ∀ (a b x : ↥(P.Lin (ZMod 4))), (πO T) x = (μ ((πO T) a)) ((πO T) b) → (μO a) b = 2 • x) {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hv : R → M) (hv_mul : ∀ (a b t : R), P.mul a b = some t → hv t = hv a + hv b) (hv_e : ∀ (x : D.PV), hv (P.e x) = 0) (hΘ : ∀ (a : R), (grA0 W ⋯ D).IsHom (hv a) (T.Θ (P.b (ZMod 2) a))) {χ : M} (hχ : ∀ (α β : M) (a b : (CatAlg.Alg D.F0)ᵐᵒᵖ), (grA0 W ⋯ D).IsHom α a → (grA0 W ⋯ D).IsHom β b → (grA0 W ⋯ D).IsHom (α + β + χ) ((μ a) b)) {h0 : ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4))} (hh0 : μO = GExt.hcobdry h0) (h01 : h0 1 = 0) : ∃ (h : ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4))), μO = GExt.hcobdry h ∧ h 1 = 0 ∧ ∀ (r : R), (P.wProjO hv (hv r + χ)) (h (P.b (ZMod 4) r)) = h (P.b (ZMod 4) r)

Lemma 10.2, in each weight: the weight-χ part of a normalized coboundary of 2μ̃ is a normalized coboundary of 2μ̃, homogeneous of weight χ.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_normalized_cobdry_weight {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {μ : Coch2 D} {μO : Coch2O P} (hμO : ∀ (a b x : ↥(P.Lin (ZMod 4))), (πO T) x = (μ ((πO T) a)) ((πO T) b) → (μO a) b = 2 • x) {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hv : R → M) (hv_mul : ∀ (a b t : R), P.mul a b = some t → hv t = hv a + hv b) (hv_e : ∀ (x : D.PV), hv (P.e x) = 0) (hΘ : ∀ (a : R), (grA0 W ⋯ D).IsHom (hv a) (T.Θ (P.b (ZMod 2) a))) {χ : M} (hχ : ∀ (α β : M) (a b : (CatAlg.Alg D.F0)ᵐᵒᵖ), (grA0 W ⋯ D).IsHom α a → (grA0 W ⋯ D).IsHom β b → (grA0 W ⋯ D).IsHom (α + β + χ) ((μ a) b)) (J : D.InjData) (h1 : DegOne D) {S : ScalarMeshCategory.RowSet Q} (hspan : ScalarMeshCategory.CokerSpan c S) (htwo : ScalarMeshCategory.TwoRows Q S) {q : ℕ} (hq : 1 ≤ q) (hμ : GExt.IsHCocycle μ) (hdeg : GExt.HDeg (galgA0 D ⋯) μ ↑q) (hn : ∀ (b : (CatAlg.Alg D.F0)ᵐᵒᵖ), (μ 1) b = 0) : ∃ (h : ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4))), μO = GExt.hcobdry h ∧ h 1 = 0 ∧ ∀ (r : R), (P.wProjO hv (hv r + χ)) (h (P.b (ZMod 4) r)) = h (P.b (ZMod 4) r)

Lemma 10.2 in every weight: for a normalized cocycle μ̄ of positive degree and character χ, 2μ̃ is the coboundary of a normalized one-cochain homogeneous of weight χ.

def MultiplicativeBasisDeformations.MeshWalk.ModFourStmt {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) : Prop

The statement of Lemma 10.2 for the table T: for every normalized Hochschild two-cocycle μ̄ of A⁽²⁾ of internal degree q > 0, every 2μ̃ is a coboundary in the normalized Hochschild complex of A⁽⁴⁾ = 𝒪P.

def MultiplicativeBasisDeformations.MeshWalk.ModFourWeightStmt {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hv : R → M) : Prop

The statement of Lemma 10.2 in every weight: for ray weights hv, if moreover μ̄ has character χ for the mesh weight W, the normalized coboundary can be chosen homogeneous of weight χ.

theorem MultiplicativeBasisDeformations.MeshWalk.modFourStmt {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) (J : D.InjData) (h1 : DegOne D) {S : ScalarMeshCategory.RowSet Q} (hspan : ScalarMeshCategory.CokerSpan c S) (htwo : ScalarMeshCategory.TwoRows Q S) : ModFourStmt T

theorem MultiplicativeBasisDeformations.MeshWalk.modFourWeightStmt {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hv : R → M) (hv_mul : ∀ (a b t : R), P.mul a b = some t → hv t = hv a + hv b) (hv_e : ∀ (x : D.PV), hv (P.e x) = 0) (hΘ : ∀ (a : R), (grA0 W ⋯ D).IsHom (hv a) (T.Θ (P.b (ZMod 2) a))) (J : D.InjData) (h1 : DegOne D) {S : ScalarMeshCategory.RowSet Q} (hspan : ScalarMeshCategory.CokerSpan c S) (htwo : ScalarMeshCategory.TwoRows Q S) : ModFourWeightStmt T W hv

Proposition 10.3: the connecting map

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.basis2 {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) : Module.Basis R (ZMod 2) (CatAlg.Alg D.F0)ᵐᵒᵖ

The basis of A⁽²⁾ transported from the ray basis.

theorem MultiplicativeBasisDeformations.MeshWalk.basis2_apply {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) (r : R) : (basis2 T) r = T.Θ (P.b (ZMod 2) r)

theorem MultiplicativeBasisDeformations.MeshWalk.πO_eq_sum {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) (a : ↥(P.Lin (ZMod 4))) : (πO T) a = ∑ r : R, Z4.red (((P.basis (ZMod 4)).repr a) r) • T.Θ (P.b (ZMod 2) r)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.redOne {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) (h : ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4))) : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[ZMod 2] (CatAlg.Alg D.F0)ᵐᵒᵖ

Reduction of a one-cochain of 𝒪P to A⁽²⁾.

theorem MultiplicativeBasisDeformations.MeshWalk.redOne_spec {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) (h : ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4))) (a : ↥(P.Lin (ZMod 4))) : (πO T) (h a) = (redOne T h) ((πO T) a)

theorem MultiplicativeBasisDeformations.MeshWalk.bilin_sum {K : Type u_1} {N : Type u_2} [CommRing K] [AddCommGroup N] [Module K N] {ι : Type u_3} (s : Finset ι) (f : N →ₗ[K] N →ₗ[K] N) (α β : ι → K) (u : ι → N) : (f (∑ r ∈ s, α r • u r)) (∑ t ∈ s, β t • u t) = ∑ r ∈ s, ∑ t ∈ s, (α r * β t) • (f (u r)) (u t)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.twiceO {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) (cb : Coch2 D) : Coch2O P

2c̃: twice a coefficient lift of a two-cochain of A⁽²⁾.

theorem MultiplicativeBasisDeformations.MeshWalk.twiceO_b {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) (cb : Coch2 D) (r t : R) : ((twiceO T cb) (P.b (ZMod 4) r)) (P.b (ZMod 4) t) = 2 • liftO T ((cb (T.Θ (P.b (ZMod 2) r))) (T.Θ (P.b (ZMod 2) t)))

theorem MultiplicativeBasisDeformations.MeshWalk.twiceO_spec {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) (cb : Coch2 D) (a b x : ↥(P.Lin (ZMod 4))) (hx : (πO T) x = (cb ((πO T) a)) ((πO T) b)) : ((twiceO T cb) a) b = 2 • x

def MultiplicativeBasisDeformations.MeshWalk.BocksteinStmt {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) : Prop

The statement of Proposition 10.3 for the table T: for every normalized two-cocycle c̄ of A⁽²⁾ of internal degree q > 0 there is a derivation δ̄ of A⁽²⁾ and a normalized lift δ over 𝒪 with dδ = 2c̃, i.e. c̄ = β(δ̄) = (dδ)/2 (the connecting map is surjective); and every other lift δ' of δ̄ gives (dδ')/2 = c̄ + dε̄, the same class.

theorem MultiplicativeBasisDeformations.MeshWalk.bockstein_of_cobdry {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {cb : Coch2 D} {δ : ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4))} (hδ : twiceO T cb = GExt.hcobdry δ) : (∀ (a b x : ↥(P.Lin (ZMod 4))), (πO T) x = (cb ((πO T) a)) ((πO T) b) → ((GExt.hcobdry δ) a) b = 2 • x) ∧ ∃ (δb : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[ZMod 2] (CatAlg.Alg D.F0)ᵐᵒᵖ), (∀ (a : ↥(P.Lin (ZMod 4))), (πO T) (δ a) = δb ((πO T) a)) ∧ (∀ (a b : (CatAlg.Alg D.F0)ᵐᵒᵖ), δb (a * b) = a * δb b + δb a * b) ∧ ∀ (δ' : ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4))), (∀ (a : ↥(P.Lin (ZMod 4))), (πO T) (δ' a) = δb ((πO T) a)) → ∃ (εb : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[ZMod 2] (CatAlg.Alg D.F0)ᵐᵒᵖ), ∀ (a b x : ↥(P.Lin (ZMod 4))), (πO T) x = (cb ((πO T) a)) ((πO T) b) + ((GExt.hcobdry εb) ((πO T) a)) ((πO T) b) → ((GExt.hcobdry δ') a) b = 2 • x

From a coboundary of 2c̃: the reduction is a derivation, and other lifts are cohomologous.

theorem MultiplicativeBasisDeformations.MeshWalk.bockstein {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) (J : D.InjData) (h1 : DegOne D) {S : ScalarMeshCategory.RowSet Q} (hspan : ScalarMeshCategory.CokerSpan c S) (htwo : ScalarMeshCategory.TwoRows Q S) : BocksteinStmt T

Proposition 10.3 (prop:integral-bockstein) for the table T.

def MultiplicativeBasisDeformations.MeshWalk.BocksteinWeightStmt {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hv : R → M) : Prop

Proposition 10.3 in every weight: if c̄ has character χ for the mesh weight W, the lift δ can be chosen homogeneous of weight χ for the ray weights hv.

theorem MultiplicativeBasisDeformations.MeshWalk.bocksteinWeight {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) (J : D.InjData) (h1 : DegOne D) {S : ScalarMeshCategory.RowSet Q} (hspan : ScalarMeshCategory.CokerSpan c S) (htwo : ScalarMeshCategory.TwoRows Q S) {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hv : R → M) (hv_mul : ∀ (a b t : R), P.mul a b = some t → hv t = hv a + hv b) (hv_e : ∀ (x : D.PV), hv (P.e x) = 0) (hΘ : ∀ (a : R), (grA0 W ⋯ D).IsHom (hv a) (T.Θ (P.b (ZMod 2) a))) : BocksteinWeightStmt T W hv