The characteristic-two step for A₀

The proof of Proposition 8.3(1) (main-theorems.tex) on A₀: with the rows S of Proposition 6.1 and their dual mesh weights, choose for each row with a nonzero class the indicator of Proposition 11.2 supplied by Corollary 10.5, form the binary family and apply Proposition 7.9 (char2_core).

Deviation (weights): the integer weights used for the characters are those of the mesh weight w = (w_R)_{R ∈ S} × length built from the dual mesh weights of Proposition 6.1 (dualWt), with values in ℤ^S × ℤ. The residual characters are then (e_R, deg), part of an evident integer basis (latBasis); this replaces Proposition 7.5 and Lemma 7.4 here (which need a connected Auslander–Reiten quiver). Corollary 10.5 is an explicit hypothesis of char2_A0; it is discharged by cor105Hyp in FinalBasis.lean.

The lattice of the dual weights

def MultiplicativeBasisDeformations.MeshWalk.DLat (ι : Type) : Type

The lattice ℤ^ι × ℤ of the dual weights (a type synonym without a decidable equality instance, so that the classical one is used throughout, as in the weight grading of A₀).

@[instance_reducible]

instance MultiplicativeBasisDeformations.MeshWalk.instAddCommGroupDLat {ι : Type} : AddCommGroup (DLat ι)

@[instance_reducible]

instance MultiplicativeBasisDeformations.MeshWalk.instModuleIntDLat {ι : Type} : Module ℤ (DLat ι)

def MultiplicativeBasisDeformations.MeshWalk.lenCoord {ι : Type} : DLat ι →+ ℤ

The length coordinate.

def MultiplicativeBasisDeformations.MeshWalk.dualWt0 {V : Type} [Quiver V] {Q : TranslationQuiver V} {ι : Type} (Wd : ι → MeshWt Q ℤ) : MeshWt Q ((ι → ℤ) × ℤ)

The mesh weight (w_R)_R × length, with values in ℤ^ι × ℤ.

def MultiplicativeBasisDeformations.MeshWalk.dualWt {V : Type} [Quiver V] {Q : TranslationQuiver V} {ι : Type} (Wd : ι → MeshWt Q ℤ) : MeshWt Q (DLat ι)

The mesh weight (w_R)_R × length.

theorem MultiplicativeBasisDeformations.MeshWalk.dualWt0_pw {V : Type} [Quiver V] {Q : TranslationQuiver V} {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) {y x : V} (p : Quiver.Path y x) : (dualWt0 Wd).pw p = (fun (i : ι) => (Wd i).pw p, ↑p.length)

theorem MultiplicativeBasisDeformations.MeshWalk.dualWt_pw {V : Type} [Quiver V] {Q : TranslationQuiver V} {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) {y x : V} (p : Quiver.Path y x) : (dualWt Wd).pw p = (fun (i : ι) => (Wd i).pw p, ↑p.length)

theorem MultiplicativeBasisDeformations.MeshWalk.rowWt_dualWt {V : Type} [Quiver V] {Q : TranslationQuiver V} {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) (R : (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) : rowWt (dualWt Wd) R = (fun (i : ι) => rowWt (Wd i) R, ↑R.snd.length - 2)

def MultiplicativeBasisDeformations.MeshWalk.shear0 {ι : Type} [Fintype ι] (ℓ : ι → ℤ) : ((ι → ℤ) × ℤ) ≃ₗ[ℤ] (ι → ℤ) × ℤ

The shear (v, m) ↦ (v, m + Σ v_i ℓ_i).

def MultiplicativeBasisDeformations.MeshWalk.shear {ι : Type} [Fintype ι] (ℓ : ι → ℤ) : ((ι → ℤ) × ℤ) ≃ₗ[ℤ] DLat ι

The shear, with values in DLat ι.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.latBasis {ι : Type} [Fintype ι] (ℓ : ι → ℤ) : Module.Basis (ι ⊕ Unit) ℤ (DLat ι)

An integer basis containing the residual characters.

theorem MultiplicativeBasisDeformations.MeshWalk.latBasis_inl {ι : Type} [Fintype ι] [DecidableEq ι] (ℓ : ι → ℤ) (i : ι) : (latBasis ℓ) (Sum.inl i) = (Pi.single i 1, ℓ i)

theorem MultiplicativeBasisDeformations.MeshWalk.prim_of_basis {L : Type} [AddCommGroup L] [DecidableEq L] {κ : Type u_1} (B : Module.Basis κ ℤ L) (j : κ) : RaySys.Sys.Prim (B j)

Basis vectors are primitive.

Homogeneity of the ray basis of A₀

theorem MultiplicativeBasisDeformations.MeshWalk.dualWt_map_snd {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)] {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) : MeshWt.map lenCoord (dualWt Wd) = lenW

theorem MultiplicativeBasisDeformations.MeshWalk.hdg_dual {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) : lenCoord.comp (MeshWt.res c D (dualWt Wd)) = MeshWt.res c D lenW

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.SysD {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) : RaySys.Sys D.PV (RayA0 D v₀) (DLat ι)

The ray system of A₀ with the dual weights.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.ΘD {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) : ↥((SysD D v₀ hF Wd).P.Lin k) ≃ₐ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ

kP ≅ A₀.

theorem MultiplicativeBasisDeformations.MeshWalk.ΘD_b {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) (t : RayA0 D v₀) : (ΘD D v₀ hF Wd) ((SysD D v₀ hF Wd).P.b k t) = (basisR D v₀ hF) t

theorem MultiplicativeBasisDeformations.MeshWalk.SysD_deg_wt {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) (t : RayA0 D v₀) {p : Quiver.Path ↑(↑t).1 ↑(↑t).2.1} (hp : (degW Q v₀).deg p = (↑t).2.2) : (SysD D v₀ hF Wd).P.deg ((SysD D v₀ hF Wd).P.wt t) = ↑p.length

theorem MultiplicativeBasisDeformations.MeshWalk.ΘD_lenHom {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) (t : RayA0 D v₀) : (lenA0 D ⋯).IsHom ((SysD D v₀ hF Wd).P.deg ((SysD D v₀ hF Wd).P.wt t)).toNat ((ΘD D v₀ hF Wd) ((SysD D v₀ hF Wd).P.b k t))

The ray basis is length-homogeneous.

theorem MultiplicativeBasisDeformations.MeshWalk.ΘD_latHom {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) (t : RayA0 D v₀) : (latA0 (dualWt Wd) ⋯ D).IsHom ((SysD D v₀ hF Wd).P.wt t) ((ΘD D v₀ hF Wd) ((SysD D v₀ hF Wd).P.b k t))

The ray basis is weight-homogeneous.

theorem MultiplicativeBasisDeformations.MeshWalk.FpA0_e_ΘD {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) (i : Fin (FpA0 D v₀ hF).m) : (FpA0 D v₀ hF).e i = (ΘD D v₀ hF Wd) ((SysD D v₀ hF Wd).P.b k ((SysD D v₀ hF Wd).P.e ((Fintype.equivFin D.PV).symm i)))

noncomputable def MultiplicativeBasisDeformations.MeshWalk.VxA0 {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) : (lenA0 D ⋯).Vertices

The vertex idempotents of A₀ as degree-zero vertices.

theorem MultiplicativeBasisDeformations.MeshWalk.VxA0_e {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) (i : Fin (VxA0 D v₀ hF Wd).n) : ∃ (x : D.PV), (VxA0 D v₀ hF Wd).e i = (ΘD D v₀ hF Wd) ((SysD D v₀ hF Wd).P.b k ((SysD D v₀ hF Wd).P.e x))

theorem MultiplicativeBasisDeformations.MeshWalk.rowWt_dual_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)] {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) {Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x} (hWd : ∀ (i j : ι), rowWt (Wd i) (Rw j) = if j = i then 1 else 0) (j : ι) : rowWt (dualWt Wd) (Rw j) = (latBasis fun (i : ι) => ↑(Rw i).snd.length - 2) (Sum.inl j)

def MultiplicativeBasisDeformations.MeshWalk.Cor105 {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) (Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) : Prop

The statement of Corollary 10.5 for A₀ with the dual weights: every residual row with a nonzero class in positive degree has a zero-supported representative with values in the stem lines (zero-supported-coverage).

theorem MultiplicativeBasisDeformations.MeshWalk.char2_A0 {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) (J : D.InjData) (h1 : DegOne D) [Fintype ↑Q.nonprojective] (Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) (hWd : ∀ (i j : ι), rowWt (Wd i) (Rw j) = if j = i then 1 else 0) (hS : ScalarMeshCategory.CokerSpan c (Set.range Rw)) (hcor : Cor105 D v₀ hF Wd Rw) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (P : PosFiltration (lenA0 D ⋯) B) : ∃ (F : PrimitiveIdempotents B) (b : Module.Basis (PrimitiveIdempotents.NonzeroRay k F) k B), IsNormedMultiplicativeBasis b ∧ F.IsRayTransversal ⇑b ∧ ∃ (ι : D.PV ≃ Fin F.m) (β : RayA0 D v₀ → B), F.IsRayPres (A0Mult D v₀ hF) ι β

The characteristic-two step on A₀ (proof of Proposition 8.3(1), with Proposition 7.9): an algebra B which is a positive filtered deformation of A₀ has a normed multiplicative ray basis, given the rows of Proposition 6.1 with dual weights and the zero-supported representatives of Corollary 10.5.

theorem MultiplicativeBasisDeformations.MeshWalk.indicator_span_A0 {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) (J : D.InjData) (h1 : DegOne D) [Fintype ↑Q.nonprojective] (Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) (hWd : ∀ (i j : ι), rowWt (Wd i) (Rw j) = if j = i then 1 else 0) (hS : ScalarMeshCategory.CokerSpan c (Set.range Rw)) (hcor : Cor105 D v₀ hF Wd Rw) : ∃ (n : ℕ) (E : Fin n → Quotient (SysD D v₀ hF Wd).pairSetoid) (qd : Fin n → ℕ), (∀ (j : Fin n), 0 < qd j ∧ LenGrading.IsRel₂ (VxA0 D v₀ hF Wd) ((SysD D v₀ hF Wd).transp k (ΘD D v₀ hF Wd) ((SysD D v₀ hF Wd).muE k (E j))) ∧ LenGrading.IsCocycle₂ ((SysD D v₀ hF Wd).transp k (ΘD D v₀ hF Wd) ((SysD D v₀ hF Wd).muE k (E j))) ∧ (lenA0 D ⋯).HasDeg₂ (qd j) ((SysD D v₀ hF Wd).transp k (ΘD D v₀ hF Wd) ((SysD D v₀ hF Wd).muE k (E j)))) ∧ ∀ (q : ℕ), 0 < q → ∀ (φ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), LenGrading.IsRel₂ (VxA0 D v₀ hF Wd) φ → (lenA0 D ⋯).HasDeg₂ q φ → LenGrading.IsCocycle₂ φ → ∃ (cf : Fin n → k) (f : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), LenGrading.IsRel₁ (VxA0 D v₀ hF Wd) f ∧ (lenA0 D ⋯).HasDeg₁ q f ∧ φ = ∑ j : Fin n with qd j = q, cf j • (SysD D v₀ hF Wd).transp k (ΘD D v₀ hF Wd) ((SysD D v₀ hF Wd).muE k (E j)) + LenGrading.cobdry k f

Remark 11.5, surjectivity: the indicator cocycles of Proposition 11.2 (transported to A₀) span HH²(A₀)_{>0}. Every normalized relative cocycle of positive internal degree q is a combination of indicators μ_{E_j} of degree q plus a relative coboundary (the indicators being normalized relative cocycles of positive degree).