Exact mesh relations for the lifted arrows (Proposition 10.1(3))

integral-deformations.tex: "The category E₄ has a quadratic scalar mesh presentation with unit coefficients reducing to the all-one presentation."

We use only the part needed later: the lifted arrows satisfy the mesh relations exactly for unit coefficients ũ reducing to c (WData.mesh_exact). The mesh error of the lifted arrows with the lifted coefficients reduces to zero, so it is twice an A⁽²⁾-map of degree two (exists_halfMap); such a map is a combination of the length-two paths at the row, and subtracting twice its coefficients corrects the mesh coefficients.

theorem MultiplicativeBasisDeformations.WLift.eq_of_ρ_eq {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {M' : Type u_4} [AddCommGroup M'] [Module (ZMod 4) M'] {MM' : GExt.GMod GΛ' M'} {MM : GExt.GMod GΛ M} {ρM : M' →+ M} {N : Type u_5} [AddCommGroup N] [Module (ZMod 2) N] {N' : Type u_6} [AddCommGroup N'] [Module (ZMod 4) N'] {NN' : GExt.GMod GΛ' N'} {NN : GExt.GMod GΛ N} {ρN : N' →+ N} (HM : IsLift MM' MM π ρM) (HN : IsLift NN' NN π ρN) (e : M' →ₗ[ZMod 4] N') (he : ∀ (m : M'), ρN (e m) = 0) {m n : M'} (h : ρM m = ρM n) : e m = e n

noncomputable def MultiplicativeBasisDeformations.WLift.halfMap {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {M' : Type u_4} [AddCommGroup M'] [Module (ZMod 4) M'] {MM' : GExt.GMod GΛ' M'} {MM : GExt.GMod GΛ M} {ρM : M' →+ M} {N : Type u_5} [AddCommGroup N] [Module (ZMod 2) N] {N' : Type u_6} [AddCommGroup N'] [Module (ZMod 4) N'] {NN' : GExt.GMod GΛ' N'} {NN : GExt.GMod GΛ N} {ρN : N' →+ N} (HM : IsLift MM' MM π ρM) (HN : IsLift NN' NN π ρN) (e : M' →ₗ[ZMod 4] N') (he : ∀ (m : M'), ρN (e m) = 0) : M →ₗ[ZMod 2] N

Half of a map reducing to zero.

theorem MultiplicativeBasisDeformations.WLift.halfMap_spec {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {M' : Type u_4} [AddCommGroup M'] [Module (ZMod 4) M'] {MM' : GExt.GMod GΛ' M'} {MM : GExt.GMod GΛ M} {ρM : M' →+ M} {N : Type u_5} [AddCommGroup N] [Module (ZMod 2) N] {N' : Type u_6} [AddCommGroup N'] [Module (ZMod 4) N'] {NN' : GExt.GMod GΛ' N'} {NN : GExt.GMod GΛ N} {ρN : N' →+ N} (HM : IsLift MM' MM π ρM) (HN : IsLift NN' NN π ρN) (e : M' →ₗ[ZMod 4] N') (he : ∀ (m : M'), ρN (e m) = 0) (m : M') : e m = HN.tw ((halfMap HM HN e he) (ρM m))

theorem MultiplicativeBasisDeformations.WLift.halfMap_act {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {M' : Type u_4} [AddCommGroup M'] [Module (ZMod 4) M'] {MM' : GExt.GMod GΛ' M'} {MM : GExt.GMod GΛ M} {ρM : M' →+ M} {N : Type u_5} [AddCommGroup N] [Module (ZMod 2) N] {N' : Type u_6} [AddCommGroup N'] [Module (ZMod 4) N'] {NN' : GExt.GMod GΛ' N'} {NN : GExt.GMod GΛ N} {ρN : N' →+ N} (HM : IsLift MM' MM π ρM) (HN : IsLift NN' NN π ρN) (e : M' →ₗ[ZMod 4] N') (he : ∀ (m : M'), ρN (e m) = 0) (hπ : IsRed GΛ' GΛ π) (hact : ∀ (m : M') (b : Λ'), e ((MM'.act m) b) = (NN'.act (e m)) b) (v : M) (a : Λ) : (halfMap HM HN e he) ((MM.act v) a) = (NN.act ((halfMap HM HN e he) v)) a

theorem MultiplicativeBasisDeformations.WLift.halfMap_deg {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {M' : Type u_4} [AddCommGroup M'] [Module (ZMod 4) M'] {MM' : GExt.GMod GΛ' M'} {MM : GExt.GMod GΛ M} {ρM : M' →+ M} {N : Type u_5} [AddCommGroup N] [Module (ZMod 2) N] {N' : Type u_6} [AddCommGroup N'] [Module (ZMod 4) N'] {NN' : GExt.GMod GΛ' N'} {NN : GExt.GMod GΛ N} {ρN : N' →+ N} (HM : IsLift MM' MM π ρM) (HN : IsLift NN' NN π ρN) (e : M' →ₗ[ZMod 4] N') (he : ∀ (m : M'), ρN (e m) = 0) {d : ℤ} (hdeg : ∀ (p : ℤ) (m : M'), MM'.gr.IsHom p m → NN'.gr.IsHom (p + d) (e m)) (p : ℤ) (v : M) (hv : MM.gr.IsHom p v) : NN.gr.IsHom (p + d) ((halfMap HM HN e he) v)

theorem MultiplicativeBasisDeformations.MeshWalk.path_length_two {V : Type} [Quiver V] {s t : V} (p : Quiver.Path s t) (hp : p.length = 2) : ∃ (y : V) (b : s ⟶ y) (a : y ⟶ t), p = b.toPath.comp a.toPath

A path of length two is a composite of two arrows.

theorem MultiplicativeBasisDeformations.MeshWalk.degreePart_two_eq {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)] (x : ↑Q.nonprojective) {F : LinearPaths.obj ↑(Q.tau x) ⟶ LinearPaths.obj ↑x} (hF : F ∈ LinearPaths.degreePart 2 ↑(Q.tau x) ↑x) : ∃ (l : (y : V) × (y ⟶ ↑x) → ZMod 2), F = ∑ a : (y : V) × (y ⟶ ↑x), l a • LinearPaths.path (((Q.mate x a.fst) a.snd).toPath.comp a.snd.toPath)

The length-two paths at a row are the mate composites.

def MultiplicativeBasisDeformations.MeshWalk.meshErr {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 : ↑Q.nonprojective) : (Fin (W.N ↑(Q.tau x)).n → ZMod 4) →ₗ[ZMod 4] Fin (W.N ↑x).n → ZMod 4

The mesh error of the lifted arrows with the Teichmüller coefficients.

theorem MultiplicativeBasisDeformations.MeshWalk.meshErr_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} (W : WData T) (x : ↑Q.nonprojective) (m : Fin (W.N ↑(Q.tau x)).n → ZMod 4) : (meshErr W x) m = ∑ a : (y : V) × (y ⟶ ↑x), Z4.lift ↑(c x a.fst a.snd) • (W.φ a.snd) ((W.φ ((Q.mate x a.fst) a.snd)) m)

theorem MultiplicativeBasisDeformations.MeshWalk.ρ_meshErr {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) (x : ↑Q.nonprojective) (m : Fin (W.N ↑(Q.tau x)).n → ZMod 4) : (WLift.ρF (W.N ↑x).β) ((meshErr W x) m) = 0

theorem MultiplicativeBasisDeformations.MeshWalk.meshErr_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) (x : ↑Q.nonprojective) (m : Fin (W.N ↑(Q.tau x)).n → ZMod 4) (b : ↥(P.Lin (ZMod 4))) : (meshErr W x) (((W.N ↑(Q.tau x)).MM.act m) b) = ((W.N ↑x).MM.act ((meshErr W x) m)) b

theorem MultiplicativeBasisDeformations.MeshWalk.meshErr_deg {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) (x : ↑Q.nonprojective) (p : ℤ) (m : Fin (W.N ↑(Q.tau x)).n → ZMod 4) (hm : (W.N ↑(Q.tau x)).MM.gr.IsHom p m) : (W.N ↑x).MM.gr.IsHom (p + 2) ((meshErr W x) m)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.meshHalf {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) (x : ↑Q.nonprojective) : CatAlg.Rep D.F0 (meshFam Q c ↑(Q.tau x)) →ₗ[ZMod 2] CatAlg.Rep D.F0 (meshFam Q c ↑x)

Half the mesh error, an A⁽²⁾-map M_{τx} → M_x.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_meshHalf_eq {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) (x : ↑Q.nonprojective) : ∃ (l : (y : V) × (y ⟶ ↑x) → ZMod 2), meshHalf W x = ∑ a : (y : V) × (y ⟶ ↑x), l a • fA D a.snd ∘ₗ fA D ((Q.mate x a.fst) a.snd)

theorem MultiplicativeBasisDeformations.MeshWalk.red_tw (a : ZMod 2) : Z4.red (Z4.tw a) = 0

theorem MultiplicativeBasisDeformations.MeshWalk.exists_meshUnits {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), (∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), Z4.red ↑(u x y a) = ↑(c x y a)) ∧ ∀ (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

Proposition 10.1(3), the relations: the lifted arrows satisfy the mesh relations exactly, for unit coefficients reducing to c. That they present E₄ is evO_surj and evO_eq_zero_iff (IntegralPresentation.lean).