Lemma 10.2 for twice a cocycle of A⁽²⁾ (Proposition 10.3)

integral-deformations.tex. For a Hochschild cocycle μ̄ of A⁽²⁾ of positive degree q, the cocycle μ̃ = 2μ̄ of 𝒪P is a coboundary (exists_hcobdry_twice): the corrections of the lifted modules and arrows are twice those of μ̄ (IntegralTransport); their mesh errors are twice a family of degree q + 2 ≥ 3, a derivative by Lemma B.2 (two_smul_mem_imageD), so an arrow change removes them; the projective corner of the lifted modules is 𝒪P (corner_surj, corner_inj), and CornerDeriv.eq_hcobdry concludes.

This is the composite j = 0 and injectivity of Ψ₄ used in the proof of Proposition 10.3, restricted to the classes i_*[μ̄], which is all that proof uses.

theorem MultiplicativeBasisDeformations.PathEval.evP_act_of {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GExt.GAlg Λ} {V : Type} [Quiver V] {N : V → Type u_3} [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] {MM : (X : V) → GExt.GMod GΛ (N X)} {φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x} (hφ : ∀ {y x : V} (a : y ⟶ x) (m : N y) (b : Λ), (φ a) (((MM y).act m) b) = ((MM x).act ((φ a) m)) b) {Y X : V} (p : Quiver.Path Y X) (m : N Y) (b : Λ) : (evP N (fun {y x : V} => φ) p) (((MM Y).act m) b) = ((MM X).act ((evP N (fun {y x : V} => φ) p) m)) b

theorem MultiplicativeBasisDeformations.PathEval.evL_act_of {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GExt.GAlg Λ} {V : Type} [Quiver V] {N : V → Type u_3} [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] {MM : (X : V) → GExt.GMod GΛ (N X)} {φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x} (hφ : ∀ {y x : V} (a : y ⟶ x) (m : N y) (b : Λ), (φ a) (((MM y).act m) b) = ((MM x).act ((φ a) m)) b) {Y X : V} (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) (m : N Y) (b : Λ) : ((evL N fun {y x : V} => φ) F) (((MM Y).act m) b) = ((MM X).act (((evL N fun {y x : V} => φ) F) m)) b

theorem MultiplicativeBasisDeformations.GExt.GMod.act_neg {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] (MM : GMod GΛ M) (m : M) (b : Λ) : (MM.act (-m)) b = -(MM.act m) b

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.NW {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} (W : WData T) (X : V) : Type

The lifted module of X.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.evO {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} (W : WData T) {Y X : V} : (LinearPaths.obj Y ⟶ LinearPaths.obj X) →ₗ[ZMod 4] NW W Y →ₗ[ZMod 4] NW W X

The evaluation of 𝒪Q on the lifted modules.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.ρW {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} (W : WData T) (X : V) : NW W X →+ CatAlg.Rep D.F0 (meshFam Q c X)

The reduction of a lifted module.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.imgk {V : Type} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {Y X : V} (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c X

The image of a path combination in C(Q, c).

theorem MultiplicativeBasisDeformations.MeshWalk.imgk_add {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} [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)] {Y X : V} (F G : LinearPaths.obj Y ⟶ LinearPaths.obj X) : imgk (F + G) = imgk F + imgk G

theorem MultiplicativeBasisDeformations.MeshWalk.imgk_smul {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} [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)] {Y X : V} (t : ZMod 2) (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) : imgk (t • F) = t • imgk F

theorem MultiplicativeBasisDeformations.MeshWalk.ρW_evP {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} (W : WData T) {Y X : V} (p : Quiver.Path Y X) (n : NW W Y) : (ρW W X) ((PathEval.evP (NW W) (fun {y x : V} => W.φ) p) n) = (rs D (ScalarMeshCategory.pathMor c p)) ((ρW W Y) n)

theorem MultiplicativeBasisDeformations.MeshWalk.ρW_evO {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} (W : WData T) {Y X : V} (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) (n : NW W Y) : (ρW W X) (((evO W) F) n) = (rs D (imgk ((LinearPaths.redP Z4.red) F))) ((ρW W Y) n)

Evaluation commutes with reduction.

theorem MultiplicativeBasisDeformations.MeshWalk.evO_act {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} (W : WData T) {Y X : V} (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) (m : NW W Y) (b : ↥(P.Lin (ZMod 4))) : ((evO W) F) (((W.N Y).MM.act m) b) = ((W.N X).MM.act (((evO W) F) m)) b

Evaluation of the mesh category over 𝒪

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.imgO {V : Type} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients (ZMod 4) Q) {Y X : V} (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) : ScalarMeshCategory.obj u Y ⟶ ScalarMeshCategory.obj u X

The image of a path combination in C(Q, ũ).

noncomputable def MultiplicativeBasisDeformations.MeshWalk.preO {V : Type} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients (ZMod 4) Q) {Y X : V} (φ : ScalarMeshCategory.obj u Y ⟶ ScalarMeshCategory.obj u X) : LinearPaths.obj Y ⟶ LinearPaths.obj X

A preimage in 𝒪Q.

theorem MultiplicativeBasisDeformations.MeshWalk.imgO_preO {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] (u : MeshCoefficients (ZMod 4) Q) {Y X : V} (φ : ScalarMeshCategory.obj u Y ⟶ ScalarMeshCategory.obj u X) : imgO u (preO u φ) = φ

noncomputable def MultiplicativeBasisDeformations.MeshWalk.evE {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} (W : WData T) (u : MeshCoefficients (ZMod 4) Q) {Y X : V} (φ : ScalarMeshCategory.obj u Y ⟶ ScalarMeshCategory.obj u X) : NW W Y →ₗ[ZMod 4] NW W X

The evaluation of C(Q, ũ) on the lifted modules.

theorem MultiplicativeBasisDeformations.MeshWalk.evO_eq_of_imgO {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} (W : WData T) {u : MeshCoefficients (ZMod 4) Q} (hmesh : ∀ (x : ↑Q.nonprojective), ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • W.φ a.snd ∘ₗ W.φ ((Q.mate x a.fst) a.snd) = 0) {Y X : V} {F G : LinearPaths.obj Y ⟶ LinearPaths.obj X} (h : imgO u F = imgO u G) : (evO W) F = (evO W) G

theorem MultiplicativeBasisDeformations.MeshWalk.evE_imgO {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} (W : WData T) {u : MeshCoefficients (ZMod 4) Q} (hmesh : ∀ (x : ↑Q.nonprojective), ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • W.φ a.snd ∘ₗ W.φ ((Q.mate x a.fst) a.snd) = 0) {Y X : V} (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) : evE W u (imgO u F) = (evO W) F

theorem MultiplicativeBasisDeformations.MeshWalk.evE_comp {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} (W : WData T) {u : MeshCoefficients (ZMod 4) Q} (hmesh : ∀ (x : ↑Q.nonprojective), ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • W.φ a.snd ∘ₗ W.φ ((Q.mate x a.fst) a.snd) = 0) {Y X Z : V} (φ : ScalarMeshCategory.obj u Y ⟶ ScalarMeshCategory.obj u X) (ψ : ScalarMeshCategory.obj u X ⟶ ScalarMeshCategory.obj u Z) : evE W u (CategoryTheory.CategoryStruct.comp φ ψ) = evE W u ψ ∘ₗ evE W u φ

theorem MultiplicativeBasisDeformations.MeshWalk.evE_add {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} (W : WData T) {u : MeshCoefficients (ZMod 4) Q} (hmesh : ∀ (x : ↑Q.nonprojective), ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • W.φ a.snd ∘ₗ W.φ ((Q.mate x a.fst) a.snd) = 0) {Y X : V} (φ ψ : ScalarMeshCategory.obj u Y ⟶ ScalarMeshCategory.obj u X) : evE W u (φ + ψ) = evE W u φ + evE W u ψ

theorem MultiplicativeBasisDeformations.MeshWalk.evE_smul {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} (W : WData T) {u : MeshCoefficients (ZMod 4) Q} (hmesh : ∀ (x : ↑Q.nonprojective), ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • W.φ a.snd ∘ₗ W.φ ((Q.mate x a.fst) a.snd) = 0) {Y X : V} (t : ZMod 4) (φ : ScalarMeshCategory.obj u Y ⟶ ScalarMeshCategory.obj u X) : evE W u (t • φ) = t • evE W u φ

theorem MultiplicativeBasisDeformations.MeshWalk.evE_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} (W : WData T) {u : MeshCoefficients (ZMod 4) Q} (hmesh : ∀ (x : ↑Q.nonprojective), ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • W.φ a.snd ∘ₗ W.φ ((Q.mate x a.fst) a.snd) = 0) {Y X : V} {κ : Type u_1} (s : Finset κ) (φ : κ → (ScalarMeshCategory.obj u Y ⟶ ScalarMeshCategory.obj u X)) : evE W u (∑ i ∈ s, φ i) = ∑ i ∈ s, evE W u (φ i)

theorem MultiplicativeBasisDeformations.MeshWalk.evE_arrowMor {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} (W : WData T) {u : MeshCoefficients (ZMod 4) Q} (hmesh : ∀ (x : ↑Q.nonprojective), ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • W.φ a.snd ∘ₗ W.φ ((Q.mate x a.fst) a.snd) = 0) {Y X : V} (a : Y ⟶ X) : evE W u (ScalarMeshCategory.arrowMor u a) = W.φ a

theorem MultiplicativeBasisDeformations.MeshWalk.evE_act {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} (W : WData T) {u : MeshCoefficients (ZMod 4) Q} (hmesh : ∀ (x : ↑Q.nonprojective), ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • W.φ a.snd ∘ₗ W.φ ((Q.mate x a.fst) a.snd) = 0) {Y X : V} (φ : ScalarMeshCategory.obj u Y ⟶ ScalarMeshCategory.obj u X) (m : NW W Y) (b : ↥(P.Lin (ZMod 4))) : (evE W u φ) (((W.N Y).MM.act m) b) = ((W.N X).MM.act ((evE W u φ) m)) b

theorem MultiplicativeBasisDeformations.MeshWalk.evE_meshDerivative {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} (W : WData T) {u : MeshCoefficients (ZMod 4) Q} (hmesh : ∀ (x : ↑Q.nonprojective), ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • W.φ a.snd ∘ₗ W.φ ((Q.mate x a.fst) a.snd) = 0) (f : ScalarMeshCategory.ArrowFamily u) (x : ↑Q.nonprojective) : evE W u (ScalarMeshCategory.meshDerivative u f x) = ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • (W.φ a.snd ∘ₗ evE W u (f ⟨↑(Q.tau x), ⟨a.fst, (Q.mate x a.fst) a.snd⟩⟩) + evE W u (f ⟨a.fst, ⟨↑x, a.snd⟩⟩) ∘ₗ W.φ ((Q.mate x a.fst) a.snd))

The mesh derivative evaluates to the first-order mesh error of an arrow change.

theorem MultiplicativeBasisDeformations.MeshWalk.ρW_evE {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} (W : WData T) {u : MeshCoefficients (ZMod 4) Q} (hmesh : ∀ (x : ↑Q.nonprojective), ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • W.φ a.snd ∘ₗ W.φ ((Q.mate x a.fst) a.snd) = 0) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), Z4.red ↑(u x y a) = ↑(c x y a)) {Y X : V} (φ : ScalarMeshCategory.obj u Y ⟶ ScalarMeshCategory.obj u X) (n : NW W Y) : (ρW W X) ((evE W u φ) n) = (rs D (ScalarMeshCategory.redE Z4.red u c φ)) ((ρW W Y) n)

Evaluation commutes with reduction, on C(Q, ũ).

The projective corner

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.eO {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) (s : D.PV) : ↥(P.Lin (ZMod 4))

The vertex idempotent ẽ_s of 𝒪P.

theorem MultiplicativeBasisDeformations.MeshWalk.πO_eO {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} (s : D.PV) : (πO T) (eO P s) = eP D s

theorem MultiplicativeBasisDeformations.MeshWalk.eO_idem {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} (s : D.PV) : eO P s * eO P s = eO P s

theorem MultiplicativeBasisDeformations.MeshWalk.sum_eO {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} : ∑ s : D.PV, eO P s = 1

theorem MultiplicativeBasisDeformations.MeshWalk.hψ1 {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)] (s : D.PV) (m : CatAlg.Rep D.F0 (meshFam Q c ↑s)) : ((gmodEv D ⋯ ↑s).act (CatAlg.unit s)) ((ψP D ⋯ s) m) = m

theorem MultiplicativeBasisDeformations.MeshWalk.hψ2 {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} (s : D.PV) (x : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (ψP D ⋯ s) (((gmodEv D ⋯ ↑s).act (CatAlg.unit s)) x) = (πO T) (eO P s) * x

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.wO {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} (W : WData T) (s : D.PV) : NW W ↑s

The generator w_s ∈ M̃_s.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.ψ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} (W : WData T) (s : D.PV) : NW W ↑s →ₗ[ZMod 4] ↥(P.Lin (ZMod 4))

The regular corner ψ̃_s : M̃_s → ẽ_s𝒪P.

theorem MultiplicativeBasisDeformations.MeshWalk.ρW_wO {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} (W : WData T) (s : D.PV) : (ρW W ↑s) (wO W s) = CatAlg.unit s

theorem MultiplicativeBasisDeformations.MeshWalk.wO_eO {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} (W : WData T) (s : D.PV) : ((W.N ↑s).MM.act (wO W s)) (eO P s) = wO W s

Yoneda at projective labels

theorem MultiplicativeBasisDeformations.MeshWalk.rs_unit_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)] {s : D.PV} {X : V} (f : ScalarMeshCategory.obj c ↑s ⟶ ScalarMeshCategory.obj c X) : (rs D f) (CatAlg.unit s) s = f

theorem MultiplicativeBasisDeformations.MeshWalk.rs_unit_eq_act {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)] {s : D.PV} {X : V} (m : CatAlg.Rep D.F0 (meshFam Q c X)) : (rs D (m s)) (CatAlg.unit s) = ((gmodEv D ⋯ X).act m) (eP D s)

Bijectivity of the corner evaluation

theorem MultiplicativeBasisDeformations.MeshWalk.ρW_evO_wO {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} (W : WData T) {s : D.PV} {X : V} (F : LinearPaths.obj ↑s ⟶ LinearPaths.obj X) : (ρW W X) (((evO W) F) (wO W s)) = (rs D (imgk ((LinearPaths.redP Z4.red) F))) (CatAlg.unit s)

theorem MultiplicativeBasisDeformations.MeshWalk.evO_wO_eO {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} (W : WData T) {s : D.PV} {X : V} (F : LinearPaths.obj ↑s ⟶ LinearPaths.obj X) : ((W.N X).MM.act (((evO W) F) (wO W s))) (eO P s) = ((evO W) F) (wO W s)

theorem MultiplicativeBasisDeformations.MeshWalk.corner_step_surj {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} (W : WData T) (s p : D.PV) (n : NW W ↑p) (hn : ((W.N ↑p).MM.act n) (eO P s) = n) : ∃ (F : LinearPaths.obj ↑s ⟶ LinearPaths.obj ↑p) (n₁ : NW W ↑p), ((W.N ↑p).MM.act n₁) (eO P s) = n₁ ∧ n = ((evO W) F) (wO W s) + 2 • n₁

theorem MultiplicativeBasisDeformations.MeshWalk.corner_surj {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} (W : WData T) (s p : D.PV) (n : NW W ↑p) (hn : ((W.N ↑p).MM.act n) (eO P s) = n) : ∃ (F : LinearPaths.obj ↑s ⟶ LinearPaths.obj ↑p), ((evO W) F) (wO W s) = n

The corner evaluation is surjective.

theorem MultiplicativeBasisDeformations.MeshWalk.corner_step_inj {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} (W : WData T) {u : MeshCoefficients (ZMod 4) Q} (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), Z4.red ↑(u x y a) = ↑(c x y a)) (s p : D.PV) {F : LinearPaths.obj ↑s ⟶ LinearPaths.obj ↑p} (hFw : (ρW W ↑p) (((evO W) F) (wO W s)) = 0) : ∃ G ∈ (CategoricalIdeal.HomIdeal.linearSpan (ZMod 4) (meshRelations u)).hom (LinearPaths.obj ↑s) (LinearPaths.obj ↑p), ∃ (H : LinearPaths.obj ↑s ⟶ LinearPaths.obj ↑p), F = G + 2 • H

theorem MultiplicativeBasisDeformations.MeshWalk.corner_inj {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} (W : WData T) {u : MeshCoefficients (ZMod 4) Q} (hmesh : ∀ (x : ↑Q.nonprojective), ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • W.φ a.snd ∘ₗ W.φ ((Q.mate x a.fst) a.snd) = 0) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), Z4.red ↑(u x y a) = ↑(c x y a)) (s p : D.PV) (F : LinearPaths.obj ↑s ⟶ LinearPaths.obj ↑p) (hFw : ((evO W) F) (wO W s) = 0) : F ∈ (CategoricalIdeal.HomIdeal.linearSpan (ZMod 4) (meshRelations u)).hom (LinearPaths.obj ↑s) (LinearPaths.obj ↑p)

The corner evaluation is injective modulo the mesh ideal.

Lemma 10.2 for twice a cocycle

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.LfO {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} (W : WData T) {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[ZMod 2] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[ZMod 2] (CatAlg.Alg D.F0)ᵐᵒᵖ} {μO : ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4))} (hμO : ∀ (a b x : ↥(P.Lin (ZMod 4))), (πO T) x = (μ ((πO T) a)) ((πO T) b) → (μO a) b = 2 • x) (Ld : LiftData D ⋯ q μ) (X : V) : GExt.ActLift μO (↑q) (W.N X).MM

The lifted actions over 𝒪, twice those of μ.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.gO {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} (W : WData T) {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[ZMod 2] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[ZMod 2] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld : LiftData D ⋯ q μ) {u : MeshCoefficients (ZMod 4) Q} (f : ScalarMeshCategory.ArrowFamily u) {y x : V} (a : y ⟶ x) : NW W y →ₗ[ZMod 4] NW W x

The arrow corrections: twice those of μ, changed by the evaluation of f.

theorem MultiplicativeBasisDeformations.MeshWalk.lift_gO {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} (W : WData T) {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[ZMod 2] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[ZMod 2] (CatAlg.Alg D.F0)ᵐᵒᵖ} {μO : ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4))} (hμO : ∀ (a b x : ↥(P.Lin (ZMod 4))), (πO T) x = (μ ((πO T) a)) ((πO T) b) → (μO a) b = 2 • x) (Ld : LiftData D ⋯ q μ) {u : MeshCoefficients (ZMod 4) Q} (hmesh : ∀ (x : ↑Q.nonprojective), ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • W.φ a.snd ∘ₗ W.φ ((Q.mate x a.fst) a.snd) = 0) (f : ScalarMeshCategory.ArrowFamily u) {y x : V} (a : y ⟶ x) : GExt.IsLiftHom (LfO W hμO Ld y) (LfO W hμO Ld x) (W.φ a) (gO W Ld f a)

theorem MultiplicativeBasisDeformations.MeshWalk.zmesh_gO {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} (W : WData T) {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[ZMod 2] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[ZMod 2] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld : LiftData D ⋯ q μ) {u : MeshCoefficients (ZMod 4) Q} (hmesh : ∀ (x : ↑Q.nonprojective), ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • W.φ a.snd ∘ₗ W.φ ((Q.mate x a.fst) a.snd) = 0) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), Z4.red ↑(u x y a) = ↑(c x y a)) (f : ScalarMeshCategory.ArrowFamily u) {G : ScalarMeshCategory.MeshFamily u} (hfD : ScalarMeshCategory.meshDerivative u f = 2 • G) (hGred : ∀ (x : ↑Q.nonprojective), ScalarMeshCategory.redE Z4.red u c (G x) = zhat Ld x) (x : ↑Q.nonprojective) : ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • (W.φ a.snd ∘ₗ gO W Ld f ((Q.mate x a.fst) a.snd) + gO W Ld f a.snd ∘ₗ W.φ ((Q.mate x a.fst) a.snd)) = 0

The first-order mesh errors vanish once f removes twice the mesh errors of μ.

theorem MultiplicativeBasisDeformations.MeshWalk.reg_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} (W : WData T) {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[ZMod 2] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[ZMod 2] (CatAlg.Alg D.F0)ᵐᵒᵖ} {μO : ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4))} (hμO : ∀ (a b x : ↥(P.Lin (ZMod 4))), (πO T) x = (μ ((πO T) a)) ((πO T) b) → (μO a) b = 2 • x) (Ld : LiftData D ⋯ q μ) (J : D.InjData) (h1 : DegOne D) (hμ : GExt.IsHCocycle μ) (hdeg : GExt.HDeg (galgA0 D ⋯) μ ↑q) (hLd : ∀ (X : V), Ld.L X = stdL J h1 hμ hdeg X) (p : D.PV) (n : NW W ↑p) (b : ↥(P.Lin (ZMod 4))) : (LfO W hμO Ld ↑p).act n b = ((W.N ↑p).MM.act (wO W p)) ((μO ((ψO W p) n)) b)

theorem MultiplicativeBasisDeformations.MeshWalk.exists_hcobdry_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} (J : D.InjData) (h1 : DegOne D) {S : ScalarMeshCategory.RowSet Q} (hspan : ScalarMeshCategory.CokerSpan c S) (htwo : ScalarMeshCategory.TwoRows Q S) {q : ℕ} (hq : 1 ≤ q) {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[ZMod 2] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[ZMod 2] (CatAlg.Alg D.F0)ᵐᵒᵖ} (hμ : GExt.IsHCocycle μ) (hdeg : GExt.HDeg (galgA0 D ⋯) μ ↑q) {μO : ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4))} (hμO : ∀ (a b x : ↥(P.Lin (ZMod 4))), (πO T) x = (μ ((πO T) a)) ((πO T) b) → (μO a) b = 2 • x) (hμOc : GExt.IsHCocycle μO) : ∃ (h : ↥(P.Lin (ZMod 4)) →ₗ[ZMod 4] ↥(P.Lin (ZMod 4))), μO = GExt.hcobdry h

Lemma 10.2 and Lemma B.2 for twice a cocycle (integral-deformations.tex): for a cocycle μ of A⁽²⁾ of positive degree, the cocycle 2μ of 𝒪P is a coboundary.