A⁽⁴⁾ = 𝒪P and its reduction to A⁽²⁾ (Proposition 10.1, the algebra)

integral-deformations.tex: "Its projective corner is A⁽²⁾ […]. Put A⁽⁴⁾ = 𝒪P, graded by length."

Setting (TabIso): a scalar mesh category over 𝔽₂ with mesh data D and a ray table P with a ray degree d and an isomorphism Θ : 𝔽₂P ≅ A⁽²⁾ taking every ray to a homogeneous element of its degree and the vertex rays to the vertex idempotents (for C⁽²⁾ this is IndSkeleton.Θ₂). Then A⁽⁴⁾ = 𝒪P is graded by the degrees of the rays (galgO), and the reduction π : 𝒪P → 𝔽₂P ≅ A⁽²⁾ is a reduction of graded algebras (isRed_πO).

theorem MultiplicativeBasisDeformations.MeshWalk.hfin2 {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] (x y : V) : FiniteDimensional (ZMod 2) (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)

structure MultiplicativeBasisDeformations.MeshWalk.TabIso {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) : Type

A ray table of A⁽²⁾: ray degrees and Θ : 𝔽₂P ≅ A⁽²⁾, homogeneous on the rays and matching the vertex idempotents.

• d : R → ℤ
• d_mul (r s t : R) : P.mul r s = some t → self.d t = self.d r + self.d s
• d_e (x : D.PV) : self.d (P.e x) = 0
• d_nonneg (r : R) : 0 ≤ self.d r
• Θ : ↥(P.Lin (ZMod 2)) ≃ₐ[ZMod 2] (CatAlg.Alg D.F0)ᵐᵒᵖ
• Θ_hom (r : R) : (lenA0 D ⋯).IsHom (self.d r).toNat (self.Θ (P.b (ZMod 2) r))
• Θ_e (x : D.PV) : self.Θ (P.b (ZMod 2) (P.e x)) = eP D x

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.galgO {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) : GExt.GAlg ↥(P.Lin (ZMod 4))

𝒪P as a graded algebra.

@[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} [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) : ↥(P.Lin (ZMod 4)) →+* (CatAlg.Alg D.F0)ᵐᵒᵖ

The reduction 𝒪P → A⁽²⁾.

theorem MultiplicativeBasisDeformations.MeshWalk.πO_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} [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) : (πO T) (P.b (ZMod 4) r) = T.Θ (P.b (ZMod 2) r)

theorem MultiplicativeBasisDeformations.MeshWalk.πO_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} [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 : ZMod 4) (x : ↥(P.Lin (ZMod 4))) : (πO T) (a • x) = Z4.red a • (πO T) x

theorem MultiplicativeBasisDeformations.MeshWalk.πO_eq_zero {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) {x : ↥(P.Lin (ZMod 4))} (h : (πO T) x = 0) (r : R) : Z4.red (((P.basis (ZMod 4)).repr x) r) = 0

theorem MultiplicativeBasisDeformations.MeshWalk.galgA0_isHom_len' {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)] (d : ℕ) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (galgA0 D ⋯).gr.IsHom (↑d) a ↔ (lenA0 D ⋯).IsHom d a

theorem MultiplicativeBasisDeformations.MeshWalk.repr_Θ_symm_eq_zero {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) (p' : ℕ) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) (ha' : (lenA0 D ⋯).IsHom p' a) (r : R) (hr : T.d r ≠ ↑p') : ((P.basis (ZMod 2)).repr (T.Θ.symm a)) r = 0

noncomputable def MultiplicativeBasisDeformations.MeshWalk.liftO {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) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) : ↥(P.Lin (ZMod 4))

A lift of an element of A⁽²⁾ to 𝒪P.

theorem MultiplicativeBasisDeformations.MeshWalk.πO_liftO {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) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (πO T) (liftO T a) = a

theorem MultiplicativeBasisDeformations.MeshWalk.liftO_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} [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) (p' : ℕ) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) (ha' : (lenA0 D ⋯).IsHom p' a) : (galgO T).gr.IsHom (↑p') (liftO T a)

theorem MultiplicativeBasisDeformations.MeshWalk.πO_lift {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) (p : ℤ) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) (ha : (galgA0 D ⋯).gr.IsHom p a) : ∃ (x' : ↥(P.Lin (ZMod 4))), (galgO T).gr.IsHom p x' ∧ (πO T) x' = a

theorem MultiplicativeBasisDeformations.MeshWalk.πO_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} [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) (p : ℤ) (x : ↥(P.Lin (ZMod 4))) (hx : (galgO T).gr.IsHom p x) : (galgA0 D ⋯).gr.IsHom p ((πO T) x)

theorem MultiplicativeBasisDeformations.MeshWalk.πO_ker {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) (x : ↥(P.Lin (ZMod 4))) (hx : (πO T) x = 0) : ∃ (y : ↥(P.Lin (ZMod 4))), x = 2 • y

theorem MultiplicativeBasisDeformations.MeshWalk.πO_ann {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) (x : ↥(P.Lin (ZMod 4))) (hx : 2 • x = 0) : (πO T) x = 0

theorem MultiplicativeBasisDeformations.MeshWalk.isRed_π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} [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) : WLift.IsRed (galgO T) (galgA0 D ⋯) (πO T)

π is a reduction of graded algebras.