Proposition 10.1(1) in all degrees and 10.1(3): the presentation of E₄

prop:fixed-integral-companion (integral-deformations.tex): (1) the Hom modules of E₄ are free over 𝒪 and E₄/2E₄ = C⁽²⁾; "the same two reductions exclude negative-degree Hom spaces"; (3) "E₄ has a quadratic scalar mesh presentation with unit coefficients reducing to the all-one presentation of C⁽²⁾".

• Evaluation over 𝔽₂ is full (rs_surj, from Proposition 2.10's evMap_surjective) and faithful (rs_inj); a graded map of degree d is the evaluation of a morphism of degree d, and there are none in negative degrees (exists_rs_of_homD, homD_eq_bot_of_neg).
• The graded Hom modules of the lifts vanish in negative degrees (homD'_eq_bot_of_neg), so (1) holds in every degree (integralHomFree_all).
• Path evaluation 𝒪Q → E₄ along the lifted arrows (evO) is onto the graded maps of every degree, by length-homogeneous path combinations (evO_surj), and its kernel is exactly the ideal of the unit mesh relations (evO_eq_zero_iff): this is the presentation (3).

Evaluation over 𝔽₂ is full

theorem MultiplicativeBasisDeformations.MeshWalk.rs_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)] {X Y : V} (g : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[ZMod 2] CatAlg.Rep D.F0 (meshFam Q c Y)) (hg : ∀ (m : CatAlg.Rep D.F0 (meshFam Q c X)) (b : (CatAlg.Alg D.F0)ᵐᵒᵖ), g (((gmodEv D ⋯ X).act m) b) = ((gmodEv D ⋯ Y).act (g m)) b) : ∃ (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y), rs D f = g

Evaluation is full (Proposition 2.10): every A⁽²⁾-linear map between evaluated modules is the evaluation of a morphism.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_rs_of_homD {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)] {X Y : V} {d : ℤ} {g : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[ZMod 2] CatAlg.Rep D.F0 (meshFam Q c Y)} (hg : g ∈ WLift.homD (gmodEv D ⋯ X) (gmodEv D ⋯ Y) d) : ∃ (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y), rs D f = g ∧ ∀ (s : ℕ), ↑s ≠ d → (ScalarMeshCategory.degProj c s X Y) f = 0

Graded maps are evaluations of morphisms of the same degree: a graded map of degree d is rs f with all length components of f other than d zero.

theorem MultiplicativeBasisDeformations.MeshWalk.homD_eq_bot_of_neg {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)] {X Y : V} {d : ℤ} (hd : d < 0) : WLift.homD (gmodEv D ⋯ X) (gmodEv D ⋯ Y) d = ⊥

No graded maps of negative degree between evaluated modules.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_rs_degreePart {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)] {X Y : V} {d : ℕ} {g : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[ZMod 2] CatAlg.Rep D.F0 (meshFam Q c Y)} (hg : g ∈ WLift.homD (gmodEv D ⋯ X) (gmodEv D ⋯ Y) ↑d) : ∃ f ∈ ScalarMeshCategory.degreePart c d X Y, rs D f = g

A graded map of degree d ≥ 0 is rs of a morphism of degree d.

theorem MultiplicativeBasisDeformations.MeshWalk.mem_homD_iff {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)] {X Y : V} {n : ℕ} (g : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[ZMod 2] CatAlg.Rep D.F0 (meshFam Q c Y)) : g ∈ WLift.homD (gmodEv D ⋯ X) (gmodEv D ⋯ Y) ↑n ↔ ∃ f ∈ ScalarMeshCategory.degreePart c n X Y, rs D f = g

C⁽²⁾ is the graded Hom category of its evaluated modules (Proposition 2.10, graded): the graded maps of degree n are exactly the evaluations of the morphisms of degree n, and evaluation is injective (rs_inj).

The lifts: negative degrees and the presentation

theorem MultiplicativeBasisDeformations.MeshWalk.homD'_eq_bot_of_neg {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) (N : (X : V) → ModLift T X) {X Y : V} {d : ℤ} (hd : d < 0) : WLift.homD' (N X).MM (N Y).MM d = ⊥

The graded Hom modules of the lifts vanish in negative degrees ("the same two reductions exclude negative-degree Hom spaces").

theorem MultiplicativeBasisDeformations.MeshWalk.homD_lift_all {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) (N : (X : V) → ModLift T X) (X Y : V) (d : ℤ) (f : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[ZMod 2] CatAlg.Rep D.F0 (meshFam Q c Y)) : f ∈ WLift.homD (gmodEv D ⋯ X) (gmodEv D ⋯ Y) d → ∃ f' ∈ WLift.homD' (N X).MM (N Y).MM d, ∀ (m : Fin (N X).n → ZMod 4), (WLift.ρF (N Y).β) (f' m) = f ((WLift.ρF (N X).β) m)

Graded maps lift in every degree: by Ext¹-vanishing for d > −2, trivially below.

theorem MultiplicativeBasisDeformations.MeshWalk.integralHomFree_all {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) (N : (X : V) → ModLift T X) (X Y : V) (d : ℤ) : (∃ (b : Module.Basis (Fin (Module.finrank (ZMod 2) ↥(WLift.homD (gmodEv D ⋯ X) (gmodEv D ⋯ Y) d))) (ZMod 4) ↥(WLift.homD' (N X).MM (N Y).MM d)), ∀ (i : Fin (Module.finrank (ZMod 2) ↥(WLift.homD (gmodEv D ⋯ X) (gmodEv D ⋯ Y) d))), (WLift.redHom ⋯ ⋯ ⋯ d) (b i) = (Module.finBasis (ZMod 2) ↥(WLift.homD (gmodEv D ⋯ X) (gmodEv D ⋯ Y) d)) i) ∧ Function.Surjective ⇑(WLift.redHom ⋯ ⋯ ⋯ d) ∧ ∀ (f : ↥(WLift.homD' (N X).MM (N Y).MM d)), (WLift.redHom ⋯ ⋯ ⋯ d) f = 0 ↔ ∃ (g : ↥(WLift.homD' (N X).MM (N Y).MM d)), f = 2 • g

Proposition 10.1(1) in every degree: the graded Hom modules of E₄ are free over 𝒪 on lifts of a basis of the graded Hom spaces over 𝔽₂, and reduction is onto with kernel 2· (both sides vanish in negative degrees).

theorem MultiplicativeBasisDeformations.MeshWalk.evP_isHom {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) {p₀ : ℤ} {m : NW W Y} (hm : (W.N Y).MM.gr.IsHom p₀ m) : (W.N X).MM.gr.IsHom (p₀ + ↑p.length) ((PathEval.evP (NW W) (fun {y x : V} => W.φ) p) m)

theorem MultiplicativeBasisDeformations.MeshWalk.evO_mem_homD' {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} {n : ℕ} {F : LinearPaths.obj Y ⟶ LinearPaths.obj X} (hF : F ∈ LinearPaths.degreePart n Y X) : (evO W) F ∈ WLift.homD' (W.N Y).MM (W.N X).MM ↑n

Path combinations of length n evaluate to graded maps of degree n.

theorem MultiplicativeBasisDeformations.MeshWalk.evO_surj_step {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) (J : D.InjData) (h1 : DegOne D) {Y X : V} {n : ℕ} {f : NW W Y →ₗ[ZMod 4] NW W X} (hf : f ∈ WLift.homD' (W.N Y).MM (W.N X).MM ↑n) : ∃ F ∈ LinearPaths.degreePart n Y X, ∃ (g : ↥(WLift.homD' (W.N Y).MM (W.N X).MM ↑n)), f = (evO W) F + 2 • ↑g

theorem MultiplicativeBasisDeformations.MeshWalk.evO_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) (J : D.InjData) (h1 : DegOne D) {Y X : V} {n : ℕ} {f : NW W Y →ₗ[ZMod 4] NW W X} (hf : f ∈ WLift.homD' (W.N Y).MM (W.N X).MM ↑n) : ∃ F ∈ LinearPaths.degreePart n Y X, (evO W) F = f

E₄ is generated by the lifted arrows: every graded map of degree n between the lifts is the evaluation of a path combination of length n.

theorem MultiplicativeBasisDeformations.MeshWalk.evO_inj_step {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)) {Y X : V} {F : LinearPaths.obj Y ⟶ LinearPaths.obj X} (hF : ∀ (m : NW W Y), (ρW W X) (((evO W) F) m) = 0) : ∃ G ∈ (CategoricalIdeal.HomIdeal.linearSpan (ZMod 4) (meshRelations u)).hom (LinearPaths.obj Y) (LinearPaths.obj X), ∃ (H : LinearPaths.obj Y ⟶ LinearPaths.obj X), F = G + 2 • H

theorem MultiplicativeBasisDeformations.MeshWalk.evO_eq_zero_iff {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} (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) : (evO W) F = 0 ↔ F ∈ (CategoricalIdeal.HomIdeal.linearSpan (ZMod 4) (meshRelations u)).hom (LinearPaths.obj Y) (LinearPaths.obj X)

The kernel of path evaluation is the ideal of the unit mesh relations: together with evO_surj, E₄ is presented by the quadratic mesh relations with coefficients u.

def MultiplicativeBasisDeformations.MeshWalk.Prop101Stmt {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.1 (prop:fixed-integral-companion) for the table T: the modules M_X⁽²⁾ lift to graded 𝒪P-modules free over 𝒪 with degree-one arrow lifts (WData), and their graded Hom category E₄ satisfies (1) its Hom modules are free over 𝒪 in every degree, with E₄/2E₄ the graded Homs of the modules of C⁽²⁾, which are the morphisms of C⁽²⁾ of the same degree; (2) at projective labels the lifts are ẽ_s𝒪P, through the generator w_s; (3) E₄ is presented by the quadratic mesh relations with unit coefficients u reducing to the all-one coefficients c: path evaluation is onto every graded Hom module (by paths of the same length) and its kernel is the ideal of the u-mesh relations.

theorem MultiplicativeBasisDeformations.MeshWalk.prop101 {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) : Prop101Stmt T

Proposition 10.1 (prop:fixed-integral-companion), for any ray table of A⁽²⁾.