Weight-homogeneous lifts for A⁽²⁾ = 𝔽₂P (Proposition 10.1)

integral-deformations.tex: "lifting a basis of H_ℤ to mesh weights by Lemma 7.4 gives the modules M_i⁽²⁾ compatible weight gradings, and the corrections can be chosen in each weight component."

For the table tab₂ of A⁽²⁾ and any mesh weight W (with values in any abelian group), the ray weights are the restriction of W (hvW, Lemma 7.4's MeshWt.rv), and the ray basis vectors Θ₂(b_r) = e_r of A⁽²⁾ are homogeneous of these weights (hΘ₂): e_r is the matrix unit of a path of the deck degree of r (eT_eq_path). So the weight-homogeneous lifts hold for A⁽²⁾ with no further hypothesis (exists_modLiftW₂, exists_arrowLiftW₂).

theorem MultiplicativeBasisDeformations.MGr.isHom_unique {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [DecidableEq M] {N : Type u_3} [AddCommGroup N] [Module R N] (G : MGr R M N) {g h : M} {n : N} (hn : n ≠ 0) (hg : G.IsHom g n) (hh : G.IsHom h n) : g = h

A nonzero homogeneous element has a unique weight.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.hvW {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [∀ (x y : S.ARVertex), Subsingleton (x ⟶ y)] (v₀ : S.ARVertex) {M : Type} [AddCommGroup M] (W : MeshWalk.MeshWt S.arTranslationQuiver M) (r : MeshWalk.RayA0 (S.arMeshData b) v₀) : M

The ray weights of a mesh weight (the restriction of Lemma 7.4).

theorem MultiplicativeBasisDeformations.IndSkeleton.exists_path_ray {k A : Type w} [Field k] [IsAlgClosed k] [CharP k 2] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [∀ (x y : S.ARVertex), Subsingleton (x ⟶ y)] [∀ (x y : S.ARVertex), FiniteDimensional k (MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) y)] [∀ (x y : S.ARVertex), FiniteDimensional (ZMod 2) (MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) y)] (v₀ : S.ARVertex) (hF : IsRepresentationFinite k (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ) (r : MeshWalk.RayA0 (S.arMeshData b) v₀) : ∃ (p : Quiver.Path ↑(↑r).1 ↑(↑r).2.1), (MeshWalk.degW S.arTranslationQuiver v₀).deg p = (↑r).2.2 ∧ ScalarMeshCategory.pathMor (S.arCoefficients b) p ≠ 0

theorem MultiplicativeBasisDeformations.IndSkeleton.eT_eq_path {k A : Type w} [Field k] [IsAlgClosed k] [CharP k 2] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [∀ (x y : S.ARVertex), Subsingleton (x ⟶ y)] [∀ (x y : S.ARVertex), FiniteDimensional k (MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) y)] [∀ (x y : S.ARVertex), FiniteDimensional (ZMod 2) (MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) y)] (v₀ : S.ARVertex) (hF : IsRepresentationFinite k (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWalk.MeshWt S.arTranslationQuiver ℤ) (r : MeshWalk.RayA0 (S.arMeshData b) v₀) {p : Quiver.Path ↑(↑r).1 ↑(↑r).2.1} (hp : (MeshWalk.degW S.arTranslationQuiver v₀).deg p = (↑r).2.2) (hp0 : ScalarMeshCategory.pathMor (S.arCoefficients b) p ≠ 0) : S.eT b v₀ hF Wd r = MulOpposite.op (CatAlg.unitM (↑r).1 (↑r).2.1 (ScalarMeshCategory.pathMor (S.oneC (ZMod 2)) p))

e_r is the matrix unit of any path of the deck degree of r with nonzero image.

theorem MultiplicativeBasisDeformations.IndSkeleton.unitM_path_isHom {k A : Type w} [Field k] [IsAlgClosed k] [CharP k 2] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [∀ (x y : S.ARVertex), Subsingleton (x ⟶ y)] [∀ (x y : S.ARVertex), FiniteDimensional k (MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) y)] [∀ (x y : S.ARVertex), FiniteDimensional (ZMod 2) (MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) y)] {M : Type} [AddCommGroup M] (W : MeshWalk.MeshWt S.arTranslationQuiver M) {x y : (S.primeMeshData b).PV} (p : Quiver.Path ↑x ↑y) : (MeshWalk.grA0 W ⋯ (S.primeMeshData b)).IsHom (W.pw p) (MulOpposite.op (CatAlg.unitM x y (ScalarMeshCategory.pathMor (S.oneC (ZMod 2)) p)))

The matrix unit of a path is homogeneous of the weight of the path.

theorem MultiplicativeBasisDeformations.IndSkeleton.eT_isHomW {k A : Type w} [Field k] [IsAlgClosed k] [CharP k 2] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [∀ (x y : S.ARVertex), Subsingleton (x ⟶ y)] [∀ (x y : S.ARVertex), FiniteDimensional k (MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) y)] [∀ (x y : S.ARVertex), FiniteDimensional (ZMod 2) (MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) y)] (v₀ : S.ARVertex) (hF : IsRepresentationFinite k (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWalk.MeshWt S.arTranslationQuiver ℤ) {M : Type} [AddCommGroup M] (W : MeshWalk.MeshWt S.arTranslationQuiver M) (r : MeshWalk.RayA0 (S.arMeshData b) v₀) : (MeshWalk.grA0 W ⋯ (S.primeMeshData b)).IsHom (S.hvW b v₀ W r) (S.eT b v₀ hF Wd r)

The basis vectors e_r of A⁽²⁾ are homogeneous for the restricted weights.

theorem MultiplicativeBasisDeformations.IndSkeleton.hΘ₂ {k A : Type w} [Field k] [IsAlgClosed k] [CharP k 2] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [∀ (x y : S.ARVertex), Subsingleton (x ⟶ y)] [∀ (x y : S.ARVertex), FiniteDimensional k (MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) y)] [∀ (x y : S.ARVertex), FiniteDimensional (ZMod 2) (MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) y)] (v₀ : S.ARVertex) (hF : IsRepresentationFinite k (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWalk.MeshWt S.arTranslationQuiver ℤ) {M : Type} [AddCommGroup M] (W : MeshWalk.MeshWt S.arTranslationQuiver M) (r : MeshWalk.RayA0 (S.arMeshData b) v₀) : (MeshWalk.grA0 W ⋯ (S.primeMeshData b)).IsHom (S.hvW b v₀ W r) ((S.tab₂ b v₀ hF Wd).Θ ((MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).P.b (ZMod 2) r))

The ray basis Θ₂(b_r) of A⁽²⁾ is homogeneous for the restricted weights.

theorem MultiplicativeBasisDeformations.IndSkeleton.hvW_mul {k A : Type w} [Field k] [IsAlgClosed k] [CharP k 2] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [∀ (x y : S.ARVertex), Subsingleton (x ⟶ y)] [∀ (x y : S.ARVertex), FiniteDimensional k (MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) y)] [∀ (x y : S.ARVertex), FiniteDimensional (ZMod 2) (MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) y)] (v₀ : S.ARVertex) (hF : IsRepresentationFinite k (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWalk.MeshWt S.arTranslationQuiver ℤ) {M : Type} [AddCommGroup M] (W : MeshWalk.MeshWt S.arTranslationQuiver M) (r s t : MeshWalk.RayA0 (S.arMeshData b) v₀) (h : (MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).P.mul r s = some t) : S.hvW b v₀ W t = S.hvW b v₀ W r + S.hvW b v₀ W s

The restricted ray weights are additive on nonzero products.

theorem MultiplicativeBasisDeformations.IndSkeleton.hvW_e {k A : Type w} [Field k] [IsAlgClosed k] [CharP k 2] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [∀ (x y : S.ARVertex), Subsingleton (x ⟶ y)] [∀ (x y : S.ARVertex), FiniteDimensional k (MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) y)] [∀ (x y : S.ARVertex), FiniteDimensional (ZMod 2) (MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) y)] (v₀ : S.ARVertex) (hF : IsRepresentationFinite k (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWalk.MeshWt S.arTranslationQuiver ℤ) {M : Type} [AddCommGroup M] (W : MeshWalk.MeshWt S.arTranslationQuiver M) (x : (S.arMeshData b).PV) : S.hvW b v₀ W ((MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).P.e x) = 0

The restricted ray weights vanish on the idempotents.

Proposition 10.1: weight-homogeneous lifts for A⁽²⁾

theorem MultiplicativeBasisDeformations.IndSkeleton.exists_modLiftW₂ {k A : Type w} [Field k] [IsAlgClosed k] [CharP k 2] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [∀ (x y : S.ARVertex), Subsingleton (x ⟶ y)] [∀ (x y : S.ARVertex), FiniteDimensional k (MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) y)] [∀ (x y : S.ARVertex), FiniteDimensional (ZMod 2) (MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) y)] (v₀ : S.ARVertex) (hF : IsRepresentationFinite k (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWalk.MeshWt S.arTranslationQuiver ℤ) {M : Type} [AddCommGroup M] (W : MeshWalk.MeshWt S.arTranslationQuiver M) {r : ℕ} (φ : Fin r → M →+ ℤ) (X : S.ARVertex) : Nonempty (MeshWalk.ModLiftW (S.tab₂ b v₀ hF Wd) W (S.hvW b v₀ W) ⋯ ⋯ φ X)

Proposition 10.1, weight-homogeneous module lifts for A⁽²⁾ = 𝔽₂P: for any mesh weight W and any finite family of integer coordinates, every evaluated module M_X⁽²⁾ lifts to 𝒪 = ℤ/4 with an action homogeneous for the degree and for every coordinate of the restricted ray weights.

theorem MultiplicativeBasisDeformations.IndSkeleton.exists_arrowLiftW₂ {k A : Type w} [Field k] [IsAlgClosed k] [CharP k 2] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [∀ (x y : S.ARVertex), Subsingleton (x ⟶ y)] [∀ (x y : S.ARVertex), FiniteDimensional k (MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) y)] [∀ (x y : S.ARVertex), FiniteDimensional (ZMod 2) (MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.oneC (ZMod 2)) y)] (v₀ : S.ARVertex) (hF : IsRepresentationFinite k (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWalk.MeshWt S.arTranslationQuiver ℤ) {M : Type} [AddCommGroup M] (W : MeshWalk.MeshWt S.arTranslationQuiver M) {r : ℕ} (φ : Fin r → M →+ ℤ) (N : (X : S.ARVertex) → MeshWalk.ModLiftW (S.tab₂ b v₀ hF Wd) W (S.hvW b v₀ W) ⋯ ⋯ φ X) {y x : S.ARVertex} (a : y ⟶ x) : ∃ (f : (Fin (N y).n → ZMod 4) →ₗ[ZMod 4] Fin (N x).n → ZMod 4), (∀ (m : Fin (N y).n → ZMod 4) (b_1 : ↥((MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).P.Lin (ZMod 4))), f (((N y).MM.act m) b_1) = ((N x).MM.act (f m)) b_1) ∧ (∀ (m : Fin (N y).n → ZMod 4), (WLift.ρF (N x).β) (f m) = (MeshWalk.fA (S.primeMeshData b) a) ((WLift.ρF (N y).β) m)) ∧ (∀ (p : ℤ) (m : Fin (N y).n → ZMod 4), (N y).MM.gr.IsHom p m → (N x).MM.gr.IsHom (p + 1) (f m)) ∧ ∀ (i : Fin r) (p : ℤ) (m : Fin (N y).n → ZMod 4), (WLift.grF ((N y).wβ i)).IsHom p m → (WLift.grF ((N x).wβ i)).IsHom (p + (φ i) (W.w a)) (f m)

Proposition 10.1, weight-homogeneous arrow lifts for A⁽²⁾ = 𝔽₂P: the arrow maps lift to maps of degree one, homogeneous of the weight of the arrow for every coordinate.