A⁽²⁾ = 𝔽₂P (Section 10)

integral-deformations.tex: "Its projective corner End(⊕_x P_x)^op is A⁽²⁾: a nonzero homogeneous projective Hom is one-dimensional over 𝔽₂, and every nonzero product coefficient is one."

The form functor of C⁽²⁾ → k(Γ_A) gives an injective ring map ι₂ : A⁽²⁾ → A₀ on the projective corners (ι₂), and 𝔽₂-independent families stay k-independent (linearIndependent_ι₂). For each ray t of A₀ (with its normed basis vector b_t) the corner of A⁽²⁾ at the endpoints of t in the length degree of t contains exactly one nonzero vector e_t (eT); ι₂ e_t is a nonzero multiple of b_t. The e_t form a multiplicative basis of A⁽²⁾ with the multiplication table of A₀, hence 𝔽₂P ≅ A⁽²⁾ (Θ₂).

noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.linOf {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (M : Mult V R) {K : Type} [Field K] {Λ : Type u_1} [Ring Λ] [Algebra K Λ] (e : Module.Basis R K Λ) : ↥(M.Lin K) ≃ₗ[K] Λ

The linear equivalence KP ≃ Λ of a basis with the multiplication table of P.

theorem MultiplicativeBasisDeformations.RaySys.Mult.linOf_b {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (M : Mult V R) {K : Type} [Field K] {Λ : Type u_1} [Ring Λ] [Algebra K Λ] (e : Module.Basis R K Λ) (r : R) : (M.linOf e) (M.b K r) = e r

theorem MultiplicativeBasisDeformations.RaySys.Mult.linOf_mul {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (M : Mult V R) {K : Type} [Field K] {Λ : Type u_1} [Ring Λ] [Algebra K Λ] (e : Module.Basis R K Λ) (he : ∀ (r s : R), e r * e s = (M.mul r s).elim 0 ⇑e) (x y : ↥(M.Lin K)) : (M.linOf e) (x * y) = (M.linOf e) x * (M.linOf e) y

noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.algOf {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (M : Mult V R) {K : Type} [Field K] {Λ : Type u_1} [Ring Λ] [Algebra K Λ] (e : Module.Basis R K Λ) (he : ∀ (r s : R), e r * e s = (M.mul r s).elim 0 ⇑e) (h1 : ∑ v : V, e (M.e v) = 1) : ↥(M.Lin K) ≃ₐ[K] Λ

An algebra with a basis carrying the multiplication table of P is KP.

theorem MultiplicativeBasisDeformations.RaySys.Mult.algOf_b {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (M : Mult V R) {K : Type} [Field K] {Λ : Type u_1} [Ring Λ] [Algebra K Λ] (e : Module.Basis R K Λ) (he : ∀ (r s : R), e r * e s = (M.mul r s).elim 0 ⇑e) (h1 : ∑ v : V, e (M.e v) = 1) (r : R) : (M.algOf e he h1) (M.b K r) = e r

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.Fm2 {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} (φ : ScalarMeshCategory.obj (S.oneC (ZMod 2)) x ⟶ ScalarMeshCategory.obj (S.oneC (ZMod 2)) y) : S.meshObj b x ⟶ S.meshObj b y

The form functor C⁽²⁾ → k(Γ_A) on morphisms.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.ret2 {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) (θ : k →ₗ[ZMod 2] ZMod 2) {x y : S.ARVertex} (ψ : S.meshObj b x ⟶ S.meshObj b y) : ScalarMeshCategory.obj (S.oneC (ZMod 2)) x ⟶ ScalarMeshCategory.obj (S.oneC (ZMod 2)) y

The retraction k(Γ_A) → C⁽²⁾ along θ.

theorem MultiplicativeBasisDeformations.IndSkeleton.Fm2_add {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} (φ φ' : ScalarMeshCategory.obj (S.oneC (ZMod 2)) x ⟶ ScalarMeshCategory.obj (S.oneC (ZMod 2)) y) : S.Fm2 b (φ + φ') = S.Fm2 b φ + S.Fm2 b φ'

theorem MultiplicativeBasisDeformations.IndSkeleton.Fm2_zero {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} : S.Fm2 b 0 = 0

theorem MultiplicativeBasisDeformations.IndSkeleton.Fm2_smul {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} (a : ZMod 2) (φ : ScalarMeshCategory.obj (S.oneC (ZMod 2)) x ⟶ ScalarMeshCategory.obj (S.oneC (ZMod 2)) y) : S.Fm2 b (a • φ) = (algebraMap (ZMod 2) k) a • S.Fm2 b φ

theorem MultiplicativeBasisDeformations.IndSkeleton.Fm2_sum {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} {κ : Type u_1} (s : Finset κ) (φ : κ → (ScalarMeshCategory.obj (S.oneC (ZMod 2)) x ⟶ ScalarMeshCategory.obj (S.oneC (ZMod 2)) y)) : S.Fm2 b (∑ i ∈ s, φ i) = ∑ i ∈ s, S.Fm2 b (φ i)

theorem MultiplicativeBasisDeformations.IndSkeleton.Fm2_comp {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 z : S.ARVertex} (φ : ScalarMeshCategory.obj (S.oneC (ZMod 2)) x ⟶ ScalarMeshCategory.obj (S.oneC (ZMod 2)) y) (φ' : ScalarMeshCategory.obj (S.oneC (ZMod 2)) y ⟶ ScalarMeshCategory.obj (S.oneC (ZMod 2)) z) : S.Fm2 b (CategoryTheory.CategoryStruct.comp φ φ') = CategoryTheory.CategoryStruct.comp (S.Fm2 b φ) (S.Fm2 b φ')

theorem MultiplicativeBasisDeformations.IndSkeleton.Fm2_id {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 : S.ARVertex} : S.Fm2 b (CategoryTheory.CategoryStruct.id (ScalarMeshCategory.obj (S.oneC (ZMod 2)) x)) = CategoryTheory.CategoryStruct.id (S.meshObj b x)

theorem MultiplicativeBasisDeformations.IndSkeleton.Fm2_injective {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} : Function.Injective (S.Fm2 b)

theorem MultiplicativeBasisDeformations.IndSkeleton.Fm2_pathMor {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} (p : Quiver.Path x y) : S.Fm2 b (ScalarMeshCategory.pathMor (S.oneC (ZMod 2)) p) = ↑(pathWt (fun {x y : S.ARVertex} => S.arMu b) p) • ScalarMeshCategory.pathMor (S.arCoefficients b) p

theorem MultiplicativeBasisDeformations.IndSkeleton.ret2_smul_Fm2 {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} (θ : k →ₗ[ZMod 2] ZMod 2) (t : k) (φ : ScalarMeshCategory.obj (S.oneC (ZMod 2)) x ⟶ ScalarMeshCategory.obj (S.oneC (ZMod 2)) y) : S.ret2 b θ (t • S.Fm2 b φ) = θ t • φ

theorem MultiplicativeBasisDeformations.IndSkeleton.ret2_add {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} (θ : k →ₗ[ZMod 2] ZMod 2) (ψ ψ' : S.meshObj b x ⟶ S.meshObj b y) : S.ret2 b θ (ψ + ψ') = S.ret2 b θ ψ + S.ret2 b θ ψ'

theorem MultiplicativeBasisDeformations.IndSkeleton.ret2_zero {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} (θ : k →ₗ[ZMod 2] ZMod 2) : S.ret2 b θ 0 = 0

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.IndSkeleton.A2 {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) : Type

The prime-field corner algebra A⁽²⁾.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.IndSkeleton.Ak {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) : Type w

The corner algebra A₀.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.ι₂ {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) (a : S.A2 b) : S.Ak b

The comparison ι₂ : A⁽²⁾ → A₀, entrywise the form functor.

theorem MultiplicativeBasisDeformations.IndSkeleton.ι₂_apply {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) (a : S.A2 b) (p q : (S.arMeshData b).PV) : MulOpposite.unop (S.ι₂ b a) p q = S.Fm2 b (MulOpposite.unop a p q)

theorem MultiplicativeBasisDeformations.IndSkeleton.ι₂_add {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) (a a' : S.A2 b) : S.ι₂ b (a + a') = S.ι₂ b a + S.ι₂ b a'

theorem MultiplicativeBasisDeformations.IndSkeleton.ι₂_zero {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) : S.ι₂ b 0 = 0

theorem MultiplicativeBasisDeformations.IndSkeleton.ι₂_smul {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) (a : ZMod 2) (x : S.A2 b) : S.ι₂ b (a • x) = (algebraMap (ZMod 2) k) a • S.ι₂ b x

theorem MultiplicativeBasisDeformations.IndSkeleton.ι₂_sum {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) {κ : Type u_1} (s : Finset κ) (f : κ → S.A2 b) : S.ι₂ b (∑ i ∈ s, f i) = ∑ i ∈ s, S.ι₂ b (f i)

theorem MultiplicativeBasisDeformations.IndSkeleton.ι₂_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) (a a' : S.A2 b) : S.ι₂ b (a * a') = S.ι₂ b a * S.ι₂ b a'

theorem MultiplicativeBasisDeformations.IndSkeleton.ι₂_one {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) : S.ι₂ b 1 = 1

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.retA {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) (θ : k →ₗ[ZMod 2] ZMod 2) (z : S.Ak b) : S.A2 b

The retraction on corner algebras.

theorem MultiplicativeBasisDeformations.IndSkeleton.retA_smul_ι₂ {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) (θ : k →ₗ[ZMod 2] ZMod 2) (t : k) (a : S.A2 b) : S.retA b θ (t • S.ι₂ b a) = θ t • a

theorem MultiplicativeBasisDeformations.IndSkeleton.retA_add {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) (θ : k →ₗ[ZMod 2] ZMod 2) (z z' : S.Ak b) : S.retA b θ (z + z') = S.retA b θ z + S.retA b θ z'

theorem MultiplicativeBasisDeformations.IndSkeleton.retA_zero {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) (θ : k →ₗ[ZMod 2] ZMod 2) : S.retA b θ 0 = 0

theorem MultiplicativeBasisDeformations.IndSkeleton.retA_sum {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) (θ : k →ₗ[ZMod 2] ZMod 2) {κ : Type u_1} (s : Finset κ) (f : κ → S.Ak b) : S.retA b θ (∑ i ∈ s, f i) = ∑ i ∈ s, S.retA b θ (f i)

theorem MultiplicativeBasisDeformations.IndSkeleton.ι₂_injective {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) : Function.Injective (S.ι₂ b)

theorem MultiplicativeBasisDeformations.IndSkeleton.linearIndependent_ι₂ {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) {κ : Type u_1} {f : κ → S.A2 b} (hf : LinearIndependent (ZMod 2) f) : LinearIndependent k fun (i : κ) => S.ι₂ b (f i)

𝔽₂-independent families stay k-independent.

The basis of A⁽²⁾ over the rays of A₀

theorem MultiplicativeBasisDeformations.IndSkeleton.ι₂_unitM {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.arMeshData b).PV} (f : ScalarMeshCategory.obj (S.oneC (ZMod 2)) ↑x ⟶ ScalarMeshCategory.obj (S.oneC (ZMod 2)) ↑y) : S.ι₂ b (MulOpposite.op (CatAlg.unitM x y f)) = MulOpposite.op (CatAlg.unitM x y (S.Fm2 b f))

theorem MultiplicativeBasisDeformations.IndSkeleton.idem_eq_unitM {ι : Type} [Fintype ι] [DecidableEq ι] {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Preadditive 𝒞] {F : ι → 𝒞} (x : ι) : CatAlg.idem x = CatAlg.unitM x x (CategoryTheory.CategoryStruct.id (F x))

theorem MultiplicativeBasisDeformations.IndSkeleton.ι₂_eP {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 : (S.arMeshData b).PV) : S.ι₂ b (MeshWalk.eP (S.primeMeshData b) x) = MeshWalk.eP (S.arMeshData b) x

theorem MultiplicativeBasisDeformations.IndSkeleton.eq_of_ι₂_mem_span {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) {a a' : S.A2 b} {z : S.Ak b} (ha : a ≠ 0) (ha' : a' ≠ 0) (h : S.ι₂ b a ∈ k ∙ z) (h' : S.ι₂ b a' ∈ k ∙ z) : a = a'

Two nonzero elements of A⁽²⁾ over the same line of A₀ are equal.

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.IndSkeleton.instFintypeRayA0ARVertexArMeshData {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)] [∀ (x y : S.ARVertex), FiniteDimensional k (MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) y)] (v₀ : S.ARVertex) : Fintype (MeshWalk.RayA0 (S.arMeshData b) v₀)

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.dP {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)] [∀ (x y : S.ARVertex), FiniteDimensional k (MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) 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₀) : ℤ

The ray degree.

theorem MultiplicativeBasisDeformations.IndSkeleton.exists_eT {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₀) : ∃ (a : S.A2 b), (MeshWalk.lenA0 (S.primeMeshData b) ⋯).IsHom (S.dP b v₀ hF Wd r).toNat a ∧ ∃ (t : k), t ≠ 0 ∧ S.ι₂ b a = t • (MeshWalk.basisR (S.arMeshData b) v₀ hF) r

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.eT {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₀) : S.A2 b

The basis vector e_t of A⁽²⁾ over the ray t of A₀.

theorem MultiplicativeBasisDeformations.IndSkeleton.eT_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)] (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₀) : (MeshWalk.lenA0 (S.primeMeshData b) ⋯).IsHom (S.dP b v₀ hF Wd r).toNat (S.eT b v₀ hF Wd r)

theorem MultiplicativeBasisDeformations.IndSkeleton.eT_line {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₀) : ∃ (t : k), t ≠ 0 ∧ S.ι₂ b (S.eT b v₀ hF Wd r) = t • (MeshWalk.basisR (S.arMeshData b) v₀ hF) r

theorem MultiplicativeBasisDeformations.IndSkeleton.eT_mem {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₀) : S.ι₂ b (S.eT b v₀ hF Wd r) ∈ k ∙ (MeshWalk.basisR (S.arMeshData b) v₀ hF) r

theorem MultiplicativeBasisDeformations.IndSkeleton.eT_ne_zero {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₀) : S.eT b v₀ hF Wd r ≠ 0

theorem MultiplicativeBasisDeformations.IndSkeleton.basisR_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 ℤ) (r s : MeshWalk.RayA0 (S.arMeshData b) v₀) : (MeshWalk.basisR (S.arMeshData b) v₀ hF) r * (MeshWalk.basisR (S.arMeshData b) v₀ hF) s = ((MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).P.mul r s).elim 0 ⇑(MeshWalk.basisR (S.arMeshData b) v₀ hF)

theorem MultiplicativeBasisDeformations.IndSkeleton.eT_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 ℤ) (r s : MeshWalk.RayA0 (S.arMeshData b) v₀) : S.eT b v₀ hF Wd r * S.eT b v₀ hF Wd s = ((MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).P.mul r s).elim 0 (S.eT b v₀ hF Wd)

The e_t multiply by the table of A₀.

theorem MultiplicativeBasisDeformations.IndSkeleton.eT_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 ℤ) (x : (S.arMeshData b).PV) : S.eT b v₀ hF Wd ((MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).P.e x) = MeshWalk.eP (S.primeMeshData b) x

theorem MultiplicativeBasisDeformations.IndSkeleton.linearIndependent_eT {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 ℤ) : LinearIndependent (ZMod 2) (S.eT b v₀ hF Wd)

theorem MultiplicativeBasisDeformations.IndSkeleton.span_eT {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 ℤ) : ⊤ ≤ Submodule.span (ZMod 2) (Set.range (S.eT b v₀ hF Wd))

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.basisT {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 ℤ) : Module.Basis (MeshWalk.RayA0 (S.arMeshData b) v₀) (ZMod 2) (S.A2 b)

The basis (e_t) of A⁽²⁾.

theorem MultiplicativeBasisDeformations.IndSkeleton.basisT_apply {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₀) : (S.basisT b v₀ hF Wd) r = S.eT b v₀ hF Wd r

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.Θ₂ {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 ℤ) : ↥((MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).P.Lin (ZMod 2)) ≃ₐ[ZMod 2] S.A2 b

𝔽₂P ≅ A⁽²⁾ (integral-deformations.tex).

theorem MultiplicativeBasisDeformations.IndSkeleton.Θ₂_b {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₀) : (S.Θ₂ b v₀ hF Wd) ((MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).P.b (ZMod 2) r) = S.eT b v₀ hF Wd r

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.tab₂ {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 ℤ) : MeshWalk.TabIso (S.primeMeshData b) (MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).P.toMult

The table of A⁽²⁾ (MeshWalk.TabIso).