Corollary 2.11: Γ_{A₀} ≅ Γ_A

graded-category.tex (cor:same-ar-quiver): "The Auslander–Reiten quivers of A₀ and A are isomorphic as translation quivers."

The evaluated modules M_x form a skeleton of ind(mod A₀) (skelA0): they are indecomposable, pairwise nonisomorphic (evA_iso_eq), and every finite-dimensional indecomposable A₀-module is one of them (evA_complete, from Proposition 2.10).

theorem MultiplicativeBasisDeformations.IndSkeleton.evA_iso_eq {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} {B : Type w} [Ring B] [Algebra k B] (ψ : B ≃ₐ[k] S.A0 b) {x y : S.ARVertex} (h : Nonempty ((evA ψ).obj (S.meshObj b x) ≅ (evA ψ).obj (S.meshObj b y))) : x = y

Distinct vertices have nonisomorphic evaluated modules.

theorem MultiplicativeBasisDeformations.IndSkeleton.rep_nontrivial {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} {B : Type w} [Ring B] [Algebra k B] (ψ : B ≃ₐ[k] S.A0 b) (x : S.ARVertex) : ∃ (m : CatAlg.Rep (S.arMeshData b).F0 (S.meshObj b x)), m ≠ 0

theorem MultiplicativeBasisDeformations.IndSkeleton.evA_complete {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} {B : Type w} [Ring B] [Algebra k B] (ψ : B ≃ₐ[k] S.A0 b) [FiniteDimensional k B] (M : RightModuleCat B) (hM : IsFiniteIndecomposable k B M) : ∃ (x : S.ARVertex), Nonempty (M ≅ (evA ψ).obj (S.meshObj b x))

Every indecomposable B-module is an evaluated module (Proposition 2.10).

The skeleton of ind(mod A₀)

theorem MultiplicativeBasisDeformations.IndSkeleton.finiteDimensional_A0 {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) : FiniteDimensional k (S.A0 b)

instance MultiplicativeBasisDeformations.IndSkeleton.instFiniteDimensionalA0 {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) : FiniteDimensional k (S.A0 b)

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.ψ₀ {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) : S.A0 b ≃ₐ[k] S.A0 b

The identity of A₀.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.skelA0 {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) : IndSkeleton k (S.A0 b)

The evaluated modules as a skeleton of ind(mod A₀).

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.θ₀ {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 : S.ARVertex) : (evA (S.ψ₀ b)).obj (S.meshObj b x) ≅ (S.skelA0 b).obj (id x)

The identification of the skeleton with the evaluation.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.ΦL {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 : Fin S.n) : (S.meshObj b (S.vertex x) ⟶ S.meshObj b (S.vertex y)) →ₗ[k] (S.skelA0 b).ind x ⟶ (S.skelA0 b).ind y

Φ as a linear map.

theorem MultiplicativeBasisDeformations.IndSkeleton.ΦL_mem_iff {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) [Finite S.ARVertex] (m : ℕ) (x y : Fin S.n) (g : S.meshObj b (S.vertex x) ⟶ S.meshObj b (S.vertex y)) : (S.ΦL b x y) g ∈ (S.skelA0 b).radPow m ((S.skelA0 b).ind x) ((S.skelA0 b).ind y) ↔ MeshWalk.Ge (S.arCoefficients b) m g

theorem MultiplicativeBasisDeformations.IndSkeleton.ΦL_surjective {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) [Finite S.ARVertex] (x y : Fin S.n) : Function.Surjective ⇑(S.ΦL b x y)

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.deg1Rad {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) [Finite S.ARVertex] (x y : Fin S.n) : ↥(ScalarMeshCategory.degreePart (S.arCoefficients b) 1 (S.vertex x) (S.vertex y)) →ₗ[k] ↥((S.skelA0 b).radPow 1 ((S.skelA0 b).ind x) ((S.skelA0 b).ind y))

Degree-one morphisms into the radical.

theorem MultiplicativeBasisDeformations.IndSkeleton.deg1Rad_coe {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) [Finite S.ARVertex] (x y : Fin S.n) (g : ↥(ScalarMeshCategory.degreePart (S.arCoefficients b) 1 (S.vertex x) (S.vertex y))) : ↑((S.deg1Rad b x y) g) = (S.ΦL b x y) ↑g

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.irrMapA0 {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) [Finite S.ARVertex] (x y : Fin S.n) : ↥(ScalarMeshCategory.degreePart (S.arCoefficients b) 1 (S.vertex x) (S.vertex y)) →ₗ[k] (S.skelA0 b).Irr ((S.skelA0 b).ind x) ((S.skelA0 b).ind y)

The irreducible maps of A₀ are the degree-one morphisms of C.

theorem MultiplicativeBasisDeformations.IndSkeleton.irrMapA0_injective {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) [Finite S.ARVertex] (x y : Fin S.n) : Function.Injective ⇑(S.irrMapA0 b x y)

theorem MultiplicativeBasisDeformations.IndSkeleton.irrMapA0_surjective {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) [Finite S.ARVertex] (x y : Fin S.n) : Function.Surjective ⇑(S.irrMapA0 b x y)

theorem MultiplicativeBasisDeformations.IndSkeleton.finrank_irr_A0 {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) [Finite S.ARVertex] (x y : Fin S.n) : Module.finrank k ((S.skelA0 b).Irr ((S.skelA0 b).ind x) ((S.skelA0 b).ind y)) = Module.finrank k (S.Irr (S.ind x) (S.ind y))

Γ_{A₀} and Γ_A have the same arrows.