Part I statements

Statements of Part I results of the manuscript (Sections 2--5), with their proofs from the foundations. The remaining Part I results are proved in the foundation files listed in docs/PAPER-CORRESPONDENCE.md.

theorem MultiplicativeBasisDeformations.nonbasicBasis {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] {e : A} (he : IsIdempotentElem e) (hfull : ∀ (a : A), a ∈ Submodule.span k {x : A | ∃ (p : A) (q : A), x = p * e * q}) (hbasic : IsBasicAlgebra he.Corner) (hB : HasNormedMultiplicativeBasis k he.Corner) : HasNormedMultiplicativeBasis k A

Lemma 2.1 (lem:nonbasic-basis). If the basic algebra of A has a normed multiplicative basis, so does A. Over any field. The basic algebra is a corner eAe for a full idempotent e (AeA = A) with eAe basic.

theorem MultiplicativeBasisDeformations.splitRepresentationTransfer {k : Type u} [Field k] {B D : Type v} [Ring B] [Algebra k B] [FiniteDimensional k B] [Ring D] [Algebra k D] [FiniteDimensional k D] (C : Subalgebra k B) (q : ↥C →ₐ[k] D) (hq : Function.Surjective ⇑q) (π : B →ₗ[k] D) (hπ : ∀ (c : ↥C), π ↑c = q c) (hbimod : ∀ (c c' : ↥C) (b : B), π (↑c * b * ↑c') = q c * π b * q c') (hB : IsRepresentationFinite k B) : IsRepresentationFinite k D

Lemma 4.6 (lem:split-representation-transfer). Let C ⊆ B be a unital inclusion, q : C ↠ D a quotient, and π : B → D a C-bimodule map with π|_C = q. If B is representation-finite, so is D. Over any field.

theorem MultiplicativeBasisDeformations.finite_twoSidedIdeals {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (hA : IsRepresentationFinite k A) : Set.univ.Finite

Lemma 3.1(1) (lem:endpoint-chains), first part. A representation-finite algebra has finitely many two-sided ideals.

theorem MultiplicativeBasisDeformations.corner_isRepresentationFinite {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (hA : IsRepresentationFinite k A) {e : A} (he : IsIdempotentElem e) : IsRepresentationFinite k he.Corner

Lemma 3.1(1) (lem:endpoint-chains), second part. Every idempotent corner eAe of a representation-finite algebra is representation-finite.

theorem MultiplicativeBasisDeformations.localCorner_truncatedPolynomial {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (hbasic : IsBasicAlgebra A) (hA : IsRepresentationFinite k A) (F : PrimitiveIdempotents A) (x : Fin F.m) : ∃ (N : ℕ), 1 ≤ N ∧ Nonempty (⋯.Corner ≃ₐ[k] Polynomial k ⧸ Ideal.span {Polynomial.X ^ N})

Lemma 3.1(2) (lem:endpoint-chains). For a basic representation-finite algebra, each local corner R_x = e_x A e_x is isomorphic to k[t]/(t^N) with N ≥ 1.

theorem MultiplicativeBasisDeformations.endpointSubbimodules_chain {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (hbasic : IsBasicAlgebra A) (hA : IsRepresentationFinite k A) (F : PrimitiveIdempotents A) (x y : Fin F.m) : IsChain (fun (x1 x2 : Submodule k A) => x1 ≤ x2) {N : Submodule k A | F.IsEndpointSubbimodule x y N} ∧ (∀ (N N' : Submodule k A), F.IsEndpointSubbimodule x y N → F.IsEndpointSubbimodule x y N' → N < N' → (∀ (N'' : Submodule k A), F.IsEndpointSubbimodule x y N'' → N ≤ N'' → N'' ≤ N' → N'' = N ∨ N'' = N') → Module.finrank k ↥N' = Module.finrank k ↥N + 1) ∧ ∀ f ∈ F.corner x y, f ≠ 0 → F.endpointSpan x y f = Submodule.span k {g : A | ∃ a ∈ F.corner x x, g = a * f} ∨ F.endpointSpan x y f = Submodule.span k {g : A | ∃ b ∈ F.corner y y, g = f * b}

Lemma 3.1(3) (lem:endpoint-chains). The R_x--R_y-subbimodules of A(x, y) form a chain with one-dimensional successive quotients, and every nonzero f generates its subbimodule from one side.

theorem MultiplicativeBasisDeformations.rayTransversal_basis {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (hbasic : IsBasicAlgebra A) (hA : IsRepresentationFinite k A) (F : PrimitiveIdempotents A) (b : PrimitiveIdempotents.NonzeroRay k F → A) (hb : F.IsRayTransversal b) : LinearIndependent k b ∧ Submodule.span k (Set.range b) = ⊤ ∧ ∀ (I : TwoSidedIdeal A) (a : A), a ∈ I ↔ a ∈ Submodule.span k (b '' {r : PrimitiveIdempotents.NonzeroRay k F | b r ∈ I})

Corollary 3.3 (cor:ray-transversal). One element from each nonzero ray, using e_x for [e_x], gives a basis of A whose intersection with every two-sided ideal is a basis of that ideal.

theorem MultiplicativeBasisDeformations.rayProduct_independent {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (hbasic : IsBasicAlgebra A) (hA : IsRepresentationFinite k A) (F : PrimitiveIdempotents A) (x y z : Fin F.m) (f f' h h' : A) (hf : f ∈ F.corner x y) (hf0 : f ≠ 0) (hh : h ∈ F.corner y z) (hh0 : h ≠ 0) (hf' : f' ∈ F.ray x y f) (hh' : h' ∈ F.ray y z h) : (f * h ∈ F.insertionSpan x y z f h ↔ f' * h' ∈ F.insertionSpan x y z f' h') ∧ (f * h ∉ F.insertionSpan x y z f h → f' * h' ≠ 0 ∧ F.ray x z (f * h) = F.ray x z (f' * h'))

Lemma 3.6 (lem:ray-product-independent). The ray product does not depend on the representatives, and a nonzero ray product has a nonzero product for every choice of representatives.

theorem MultiplicativeBasisDeformations.rayDegree_radical {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (hbasic : IsBasicAlgebra A) (hA : IsRepresentationFinite k A) (F : PrimitiveIdempotents A) (x y : Fin F.m) : (∀ (d : ℕ), Module.finrank k ↥(F.corner x y ⊓ radFilt k A d) ≤ Module.finrank k ↥(F.corner x y ⊓ radFilt k A (d + 1)) + 1) ∧ (∀ (f g : A) (d : ℕ), f ∈ F.corner x y → g ∈ F.corner x y → f ∈ radFilt k A d → f ∉ radFilt k A (d + 1) → g ∈ radFilt k A d → g ∉ radFilt k A (d + 1) → F.ray x y f = F.ray x y g) ∧ ∀ (f g : A), f ∈ F.corner x y → g ∈ F.corner x y → F.endpointSpan x y g < F.endpointSpan x y f → ∀ (d d' : ℕ), f ∈ radFilt k A d → g ∈ radFilt k A d' → g ∉ radFilt k A (d' + 1) → d < d'

The algebra-radical analogue of Lemma 3.7: in a corner V = A(x, y) with F^dV = V ∩ (rad A)^d, every layer has dimension at most one, elements of the same degree lie in the same ray, and U_{r'} ⊊ U_r forces a larger degree. These layers are not the pieces A₀(x,y)_d (Example 2.12); Lemma 3.7 itself, for the categorical filtration J^d, is rayDegree.

theorem MultiplicativeBasisDeformations.projectiveRayProduct {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (G : LenGrading k A) (F : PrimitiveIdempotents A) (he0 : ∀ (x : Fin F.m), G.IsHom 0 (F.e x)) (hcorner0 : ∀ (x : Fin F.m), ∀ a ∈ F.corner x x, G.IsHom 0 a → ∃ (c : k), a = c • F.e x) (hA : IsRepresentationFinite k A) : (∀ (x y : Fin F.m), ∀ f ∈ F.corner x y, f ≠ 0 → ∃ (g : A) (d : ℕ), G.IsHom d g ∧ g ≠ 0 ∧ g ∈ F.ray x y f ∧ ∀ g' ∈ F.ray x y f, ∀ (d' : ℕ), G.IsHom d' g' → g' ∈ k ∙ g) ∧ (∀ (x y z : Fin F.m) (f h : A) (p q : ℕ), G.IsHom p f → G.IsHom q h → (f * h ∈ F.insertionSpan x y z f h ↔ f * h = 0)) ∧ ∀ (x y z w : Fin F.m) (f g h : A), f ∈ F.corner x y → f ≠ 0 → g ∈ F.corner y z → g ≠ 0 → h ∈ F.corner z w → h ≠ 0 → (f * g ∉ F.insertionSpan x y z f g ∧ f * g * h ∉ F.insertionSpan x z w (f * g) h ↔ g * h ∉ F.insertionSpan y z w g h ∧ f * (g * h) ∉ F.insertionSpan x y w f (g * h))

Proposition 3.8 (prop:projective-ray-product), for a length-graded representation-finite algebra whose idempotents have degree 0 and whose degree-0 local corners are k e_x (the case of A₀, see lenA0). (1) Each nonzero ray contains the nonzero vectors of a unique homogeneous line. (2) For homogeneous f, h, fh ∈ M(f, h) iff fh = 0. (3) The ray table is associative: ([f][g])[h] ≠ 0 iff [f]([g][h]) ≠ 0, both being [fgh].

theorem MultiplicativeBasisDeformations.posetWeights {k : Type u} [Field k] [IsAlgClosed k] {P : Type v} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] (hP : IsRepresentationFinite k (IncidenceAlgebra k P)) {G : Type w} [AddCommGroup G] (wt : P → P → G) (hwt : ∀ (x y z : P), x ≤ y → y ≤ z → wt x z = wt x y + wt y z) : ∃ (ζ : P → G), ∀ (x y : P), x ≤ y → wt x y = ζ y - ζ x

Lemma 4.9 (lem:poset-weights). If the incidence algebra of a finite poset is representation-finite, every additive weight is a difference of object values.

theorem MultiplicativeBasisDeformations.meshCorrectionSpaces {k : Type u} [Field k] [IsAlgClosed k] {V : Type v} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] (Q : TranslationQuiver V) (hQ : HasAtMostOneArrow V) (c : MeshCoefficients k Q) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (hchar : ringChar k ≠ 2) (hbrick : ScalarMeshCategory.BrickHypothesis c) (m : ℕ) (hm : 2 ≤ m) : ScalarMeshCategory.MeshDerivativeSurjective c m

Proposition 5.3 (prop:mesh-correction-spaces). For a finite-dimensional scalar mesh category on a finite translation quiver with at most one arrow between ordered vertices, satisfying the brick hypothesis, and char k ≠ 2, the derivative D_m is surjective for every m ≥ 2.

theorem MultiplicativeBasisDeformations.squareFree {k A : Type u'} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x y : Fin S.n) : Module.finrank k (S.Irr (S.ind x) (S.ind y)) ≤ 1 ∧ Module.finrank k (S.Irr (S.ind x) (S.ind x)) = 0

Lemma 2.2 (lem:square-free). The Auslander--Reiten quiver of a representation-finite algebra has no loops and at most one arrow between each ordered pair of vertices. Proved in Foundations/SquareFree.lean. (The instance IsNoetherianRing Aᵐᵒᵖ follows from finite-dimensionality, by IsNoetherianRing.of_finite.)

theorem MultiplicativeBasisDeformations.gradedRealization {k A : Type u'} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (hbasic : IsBasicAlgebra A) (S : IndSkeleton k A) (b : S.ArrowBases) : (∀ (x y : S.ARVertex), DirectSum.IsInternal fun (d : ℕ) => ScalarMeshCategory.degreePart (S.arCoefficients b) d x y) ∧ ∃ (φ : (d : ℕ) → (x y : S.ARVertex) → ↥(ScalarMeshCategory.degreePart (S.arCoefficients b) d x y) ≃ₗ[k] S.layer d (S.label x) (S.label y)), (∀ (x y : S.ARVertex) (a : x ⟶ y) (ha : ScalarMeshCategory.arrowMor (S.arCoefficients b) a ∈ ScalarMeshCategory.degreePart (S.arCoefficients b) 1 x y), (φ 1 x y) ⟨ScalarMeshCategory.arrowMor (S.arCoefficients b) a, ha⟩ = (b x y) a) ∧ ∀ (d e : ℕ) (x y z : S.ARVertex) (f : ↥(ScalarMeshCategory.degreePart (S.arCoefficients b) d x y)) (g : ↥(ScalarMeshCategory.degreePart (S.arCoefficients b) e y z)) (f' : S.label x ⟶ S.label y) (hf' : f' ∈ S.radPow d (S.label x) (S.label y)) (g' : S.label y ⟶ S.label z) (hg' : g' ∈ S.radPow e (S.label y) (S.label z)), (φ d x y) f = S.layerClass f' hf' → (φ e y z) g = S.layerClass g' hg' → ∃ (hfg : CategoryTheory.CategoryStruct.comp ↑f ↑g ∈ ScalarMeshCategory.degreePart (S.arCoefficients b) (d + e) x z) (hfg' : CategoryTheory.CategoryStruct.comp f' g' ∈ S.radPow (d + e) (S.label x) (S.label z)), (φ (d + e) x z) ⟨CategoryTheory.CategoryStruct.comp ↑f ↑g, hfg⟩ = S.layerClass (CategoryTheory.CategoryStruct.comp f' g') hfg'

Proposition 2.6(3) (prop:graded-realization). The chosen arrow classes induce an isomorphism of graded categories k(Γ_A) ≅ gr_J ind(mod A), with the scalar relations of eq:scalar-mesh. Formally: the Hom spaces of k(Γ_A) are the internal direct sums of their path-degree parts; in each degree d there is a linear isomorphism φ_d onto the radical layer J^d / J^{d+1}; φ_1 sends each arrow to its chosen basis vector of Irr; and the φ_d are compatible with composition, which in gr_J is computed on representatives.

theorem MultiplicativeBasisDeformations.unitMeshCoefficients {k A : Type u'} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (c : MeshCoefficients k S.arTranslationQuiver) : ∃ (φ : MeshWalk.Arr S.ARVertex → kˣ) (ψ : ↑S.arTranslationQuiver.nonprojective → kˣ), ∀ (x : ↑S.arTranslationQuiver.nonprojective) (y : S.ARVertex) (a : y ⟶ ↑x), c x y a * φ ⟨↑(S.arTranslationQuiver.tau x), ⟨y, (S.arTranslationQuiver.mate x y) a⟩⟩ * φ ⟨y, ⟨↑x, a⟩⟩ = ψ x

Lemma 4.4 (lem:unit-mesh-coefficients). Every coefficient system on Γ_A can be changed to coefficients one by rescaling arrows (φ) and entire mesh relations (ψ): c_{x,a} φ(σa) φ(a) = ψ(x). In every characteristic.

theorem MultiplicativeBasisDeformations.gradedStandardForm {k A : Type u'} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (hbasic : IsBasicAlgebra A) : (∀ (b : S.ArrowBases), IsRepresentationFinite k (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ) ∧ (S.IsStandard → ∃ (b : S.ArrowBases), Nonempty (A ≃ₐ[k] (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ))

Corollary 4.15 (cor:graded-standard-form), the parts used outside characteristic two: A₀ (for any choice of arrow classes) is representation-finite, and a standard basic A is isomorphic to A₀. (The converse, A ≅ A₀ ⟹ A standard, is used only in Part III, Theorem 11.8; here Theorem B obtains standardness directly from Proposition 5.4.)

theorem MultiplicativeBasisDeformations.rayDegree {k A : Type u'} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) {n : ℕ} {e : Fin n → A} (he : CompleteOrthogonalIdempotents e) (hprim : ∀ (i : Fin n), IsPrimitiveIdempotent (e i)) (hbasic : ∀ (i j : Fin n), (∃ (x : A) (y : A), e i * x * e j = x ∧ e j * y * e i = y ∧ x * y = e i ∧ y * x = e j) → i = j) (hA : IsRepresentationFinite k A) (F : PrimitiveIdempotents A) (x y : Fin F.m) : have P := S.posFiltA b he hprim hbasic; (∀ (d : ℕ), Module.finrank k ↥(P.piece F x y d) ≤ 1) ∧ (∀ (f : A) (d : ℕ), f ∈ F.corner x y → f ∈ P.F d → f ∉ P.F (d + 1) → (P.σ d) f ≠ 0 ∧ P.piece F x y d = k ∙ (P.σ d) f) ∧ (∀ (f g : A) (d d' : ℕ), f ∈ F.corner x y → g ∈ F.corner x y → f ∈ P.F d → f ∉ P.F (d + 1) → g ∈ P.F d' → g ∉ P.F (d' + 1) → (F.ray x y f = F.ray x y g ↔ d = d')) ∧ (∀ (d : ℕ), P.piece F x y d ≠ ⊥ → ∃ f ∈ F.corner x y, f ∈ P.F d ∧ f ∉ P.F (d + 1)) ∧ ∀ (f g : A), f ∈ F.corner x y → g ∈ F.corner x y → F.endpointSpan x y g < F.endpointSpan x y f → ∀ (d d' : ℕ), f ∈ P.F d → g ∈ P.F d' → g ∉ P.F (d' + 1) → d < d'

Lemma 3.7 (lem:ray-degree), for the categorical filtration F^dA(x,y) = J^d(P_y,P_x) (posFiltA, transported to A along a complete set e of primitive idempotents): every piece A₀(x,y)_d has dimension at most one; initial forms give a bijection between the nonzero rays of a corner and its nonzero pieces (a nonzero element of degree d has initial form spanning A₀(x,y)_d; same ray iff same degree; every nonzero piece is reached); and U_{r'} ⊊ U_r forces deg_J r' > deg_J r.