The converse of Corollary 4.15: A ≅ A₀ implies that A is standard

scalar-normalization.tex: "Conversely an isomorphism A ≅ A₀ gives an equivalence F : ind(mod A) → C, possibly permuting labels. Since C is generated in degree one with homogeneous relations, gr_J C = C. Thus gr F is a graded automorphism of C with the same permutation. Applying (gr F)⁻¹ after F gives the required object-preserving equivalence."

An isomorphism ψ : A ≅ A₀ makes the evaluated modules M_x of C = k(Γ_A) into indecomposable A-modules, which identifies C with ind(mod A) up to a permutation σ of the labels (Φ). Under Φ the radical powers of ind(mod A) are the morphisms of degree at least m of C (gr_J C = C, MeshRadical). Deviation: instead of correcting F by (gr F)⁻¹, the degree-one parts of the arrow representatives are taken as lifts; their mesh errors are of degree two and lie in J³, so they vanish, and the filtered normal form (Lifts.functor) gives the object-preserving equivalence (isStandard_of_algEquiv).

@[reducible, inline]

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

The algebra A₀ of A.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.eOp {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) : Bᵐᵒᵖ ≃+* CatAlg.Alg (S.arMeshData b).F0

Bᵐᵒᵖ ≅ Alg F₀.

theorem MultiplicativeBasisDeformations.IndSkeleton.eOp_algebraMap {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) (t : k) : (eOp ψ) ((algebraMap k Bᵐᵒᵖ) t) = (algebraMap k (CatAlg.Alg (S.arMeshData b).F0)) t

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.ev {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) : CategoryTheory.Functor (S.ARMeshCategory b) (ModuleCat (CatAlg.Alg (S.arMeshData b).F0))

The evaluation C → mod A₀.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.evA {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) : CategoryTheory.Functor (S.ARMeshCategory b) (RightModuleCat B)

The evaluation C → mod B through ψ.

theorem MultiplicativeBasisDeformations.IndSkeleton.evA_map_apply {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.ARMeshCategory b} (f : X ⟶ Y) (m : CatAlg.Rep (S.arMeshData b).F0 X) : (ModuleCat.Hom.hom ((evA ψ).map f)) m = (CatAlg.repMap f) m

theorem MultiplicativeBasisDeformations.IndSkeleton.evA_smul {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.ARMeshCategory b} (t : k) (m : CatAlg.Rep (S.arMeshData b).F0 X) : (t • have this := m; this) = t • m

The k-action on an evaluated A-module is the natural one.

theorem MultiplicativeBasisDeformations.IndSkeleton.evA_map_add {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.ARMeshCategory b} (f g : X ⟶ Y) : (evA ψ).map (f + g) = (evA ψ).map f + (evA ψ).map g

theorem MultiplicativeBasisDeformations.IndSkeleton.evA_map_sub {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.ARMeshCategory b} (f g : X ⟶ Y) : (evA ψ).map (f - g) = (evA ψ).map f - (evA ψ).map g

theorem MultiplicativeBasisDeformations.IndSkeleton.evA_map_smul {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.ARMeshCategory b} (t : k) (f : X ⟶ Y) : (evA ψ).map (t • f) = t • (evA ψ).map f

theorem MultiplicativeBasisDeformations.IndSkeleton.evA_map_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} {B : Type w} [Ring B] [Algebra k B] (ψ : B ≃ₐ[k] S.A0 b) (x y : S.ARVertex) : Function.Injective fun (f : S.meshObj b x ⟶ S.meshObj b y) => (evA ψ).map f

theorem MultiplicativeBasisDeformations.IndSkeleton.evA_map_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} {B : Type w} [Ring B] [Algebra k B] (ψ : B ≃ₐ[k] S.A0 b) (x y : S.ARVertex) (g : (evA ψ).obj (S.meshObj b x) ⟶ (evA ψ).obj (S.meshObj b y)) : ∃ (f : S.meshObj b x ⟶ S.meshObj b y), (evA ψ).map f = g

theorem MultiplicativeBasisDeformations.IndSkeleton.evA_id_ne_zero {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) : CategoryTheory.CategoryStruct.id ((evA ψ).obj (S.meshObj b x)) ≠ 0

instance MultiplicativeBasisDeformations.IndSkeleton.evA_isLocalRing {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) : IsLocalRing (CategoryTheory.End ((evA ψ).obj (S.meshObj b x)))

theorem MultiplicativeBasisDeformations.IndSkeleton.evA_isFiniteIndecomposable {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) : IsFiniteIndecomposable k B ((evA ψ).obj (S.meshObj b x))

The evaluated modules are finite-dimensional indecomposable A-modules.

The comparison with a skeleton

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.Φm {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) (S' : IndSkeleton k B) (σ : S.ARVertex → Fin S'.n) (θ : (x : S.ARVertex) → (evA ψ).obj (S.meshObj b x) ≅ S'.obj (σ x)) {x y : S.ARVertex} (f : S.meshObj b x ⟶ S.meshObj b y) : S'.ind (σ x) ⟶ S'.ind (σ y)

The comparison C(x, y) → ind(mod A)(σ x, σ y).

theorem MultiplicativeBasisDeformations.IndSkeleton.Φm_hom {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) (S' : IndSkeleton k B) (σ : S.ARVertex → Fin S'.n) (θ : (x : S.ARVertex) → (evA ψ).obj (S.meshObj b x) ≅ S'.obj (σ x)) {x y : S.ARVertex} (f : S.meshObj b x ⟶ S.meshObj b y) : (Φm ψ S' σ θ f).hom = CategoryTheory.CategoryStruct.comp (θ x).inv (CategoryTheory.CategoryStruct.comp ((evA ψ).map f) (θ y).hom)

theorem MultiplicativeBasisDeformations.IndSkeleton.Φm_comp {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) (S' : IndSkeleton k B) (σ : S.ARVertex → Fin S'.n) (θ : (x : S.ARVertex) → (evA ψ).obj (S.meshObj b x) ≅ S'.obj (σ x)) {x y z : S.ARVertex} (f : S.meshObj b x ⟶ S.meshObj b y) (g : S.meshObj b y ⟶ S.meshObj b z) : Φm ψ S' σ θ (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (Φm ψ S' σ θ f) (Φm ψ S' σ θ g)

theorem MultiplicativeBasisDeformations.IndSkeleton.Φm_id {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) (S' : IndSkeleton k B) (σ : S.ARVertex → Fin S'.n) (θ : (x : S.ARVertex) → (evA ψ).obj (S.meshObj b x) ≅ S'.obj (σ x)) (x : S.ARVertex) : Φm ψ S' σ θ (CategoryTheory.CategoryStruct.id (S.meshObj b x)) = CategoryTheory.CategoryStruct.id (S'.ind (σ x))

theorem MultiplicativeBasisDeformations.IndSkeleton.Φm_add {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) (S' : IndSkeleton k B) (σ : S.ARVertex → Fin S'.n) (θ : (x : S.ARVertex) → (evA ψ).obj (S.meshObj b x) ≅ S'.obj (σ x)) {x y : S.ARVertex} (f g : S.meshObj b x ⟶ S.meshObj b y) : Φm ψ S' σ θ (f + g) = Φm ψ S' σ θ f + Φm ψ S' σ θ g

theorem MultiplicativeBasisDeformations.IndSkeleton.Φm_sub {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) (S' : IndSkeleton k B) (σ : S.ARVertex → Fin S'.n) (θ : (x : S.ARVertex) → (evA ψ).obj (S.meshObj b x) ≅ S'.obj (σ x)) {x y : S.ARVertex} (f g : S.meshObj b x ⟶ S.meshObj b y) : Φm ψ S' σ θ (f - g) = Φm ψ S' σ θ f - Φm ψ S' σ θ g

theorem MultiplicativeBasisDeformations.IndSkeleton.Φm_smul {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) (S' : IndSkeleton k B) (σ : S.ARVertex → Fin S'.n) (θ : (x : S.ARVertex) → (evA ψ).obj (S.meshObj b x) ≅ S'.obj (σ x)) {x y : S.ARVertex} (t : k) (f : S.meshObj b x ⟶ S.meshObj b y) : Φm ψ S' σ θ (t • f) = t • Φm ψ S' σ θ f

theorem MultiplicativeBasisDeformations.IndSkeleton.Φm_zero {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) (S' : IndSkeleton k B) (σ : S.ARVertex → Fin S'.n) (θ : (x : S.ARVertex) → (evA ψ).obj (S.meshObj b x) ≅ S'.obj (σ x)) {x y : S.ARVertex} : Φm ψ S' σ θ 0 = 0

theorem MultiplicativeBasisDeformations.IndSkeleton.Φm_sum {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) (S' : IndSkeleton k B) (σ : S.ARVertex → Fin S'.n) (θ : (x : S.ARVertex) → (evA ψ).obj (S.meshObj b x) ≅ S'.obj (σ x)) {x y : S.ARVertex} {ι : Type u_1} (s : Finset ι) (f : ι → (S.meshObj b x ⟶ S.meshObj b y)) : Φm ψ S' σ θ (∑ i ∈ s, f i) = ∑ i ∈ s, Φm ψ S' σ θ (f i)

theorem MultiplicativeBasisDeformations.IndSkeleton.Φm_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} {B : Type w} [Ring B] [Algebra k B] (ψ : B ≃ₐ[k] S.A0 b) (S' : IndSkeleton k B) (σ : S.ARVertex → Fin S'.n) (θ : (x : S.ARVertex) → (evA ψ).obj (S.meshObj b x) ≅ S'.obj (σ x)) {x y : S.ARVertex} : Function.Injective (Φm ψ S' σ θ)

theorem MultiplicativeBasisDeformations.IndSkeleton.Φm_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} {B : Type w} [Ring B] [Algebra k B] (ψ : B ≃ₐ[k] S.A0 b) (S' : IndSkeleton k B) (σ : S.ARVertex → Fin S'.n) (θ : (x : S.ARVertex) → (evA ψ).obj (S.meshObj b x) ≅ S'.obj (σ x)) {x y : S.ARVertex} (h : S'.ind (σ x) ⟶ S'.ind (σ y)) : ∃ (f : S.meshObj b x ⟶ S.meshObj b y), Φm ψ S' σ θ f = h

theorem MultiplicativeBasisDeformations.IndSkeleton.isIso_Φm_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} {B : Type w} [Ring B] [Algebra k B] (ψ : B ≃ₐ[k] S.A0 b) (S' : IndSkeleton k B) (σ : S.ARVertex → Fin S'.n) (θ : (x : S.ARVertex) → (evA ψ).obj (S.meshObj b x) ≅ S'.obj (σ x)) {x : S.ARVertex} (f : S.meshObj b x ⟶ S.meshObj b x) : CategoryTheory.IsIso (Φm ψ S' σ θ f) ↔ CategoryTheory.IsIso f

theorem MultiplicativeBasisDeformations.IndSkeleton.σ_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} {B : Type w} [Ring B] [Algebra k B] (ψ : B ≃ₐ[k] S.A0 b) (S' : IndSkeleton k B) (σ : S.ARVertex → Fin S'.n) (θ : (x : S.ARVertex) → (evA ψ).obj (S.meshObj b x) ≅ S'.obj (σ x)) [Finite S.ARVertex] : Function.Injective σ

Radical powers are degrees

theorem MultiplicativeBasisDeformations.IndSkeleton.isRadical_Φm_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} {B : Type w} [Ring B] [Algebra k B] (ψ : B ≃ₐ[k] S.A0 b) (S' : IndSkeleton k B) (σ : S.ARVertex → Fin S'.n) (θ : (x : S.ARVertex) → (evA ψ).obj (S.meshObj b x) ≅ S'.obj (σ x)) [Finite S.ARVertex] {x y : S.ARVertex} (f : S.meshObj b x ⟶ S.meshObj b y) : S'.IsRadical (Φm ψ S' σ θ f) ↔ (ScalarMeshCategory.degProj (S.arCoefficients b) 0 x y) f = 0

theorem MultiplicativeBasisDeformations.IndSkeleton.path_first {V : Type} [Quiver V] {x y : V} (p : Quiver.Path x y) (hp : 0 < p.length) : ∃ (z : V) (a : x ⟶ z) (p' : Quiver.Path z y), p = a.toPath.comp p' ∧ p'.length + 1 = p.length

theorem MultiplicativeBasisDeformations.IndSkeleton.mem_radPow_Φm_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} {B : Type w} [Ring B] [Algebra k B] (ψ : B ≃ₐ[k] S.A0 b) (S' : IndSkeleton k B) {σ : S.ARVertex → Fin S'.n} (θ : (x : S.ARVertex) → (evA ψ).obj (S.meshObj b x) ≅ S'.obj (σ x)) [Finite S.ARVertex] (hσ : Function.Bijective σ) (m : ℕ) {x y : S.ARVertex} (f : S.meshObj b x ⟶ S.meshObj b y) : Φm ψ S' σ θ f ∈ S'.radPow m (S'.ind (σ x)) (S'.ind (σ y)) ↔ MeshWalk.Ge (S.arCoefficients b) m f

Under Φ, the radical powers are the morphisms of degree at least m.

The relabelling of ind(mod A)

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} (ψ : A ≃ₐ[k] S.A0 b) (x : S.ARVertex) : Fin S.n

The label of the evaluated module of x.

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} (ψ : A ≃ₐ[k] S.A0 b) (x : S.ARVertex) : (evA ψ).obj (S.meshObj b x) ≅ S.obj (σl ψ x)

M_x ≅ X_{σ x}.

theorem MultiplicativeBasisDeformations.IndSkeleton.σl_bijective {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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] : Function.Bijective (σl ψ)

Degree-one lifts and standardness

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.σe {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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] : S.ARVertex ≃ Fin S.n

The relabelling as an equivalence.

theorem 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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] (v : S.ARVertex) : S.ind (σl ψ ((σe ψ).symm v)) = S.label v

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.cv {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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] {v w : S.ARVertex} (h : S.ind (σl ψ ((σe ψ).symm v)) ⟶ S.ind (σl ψ ((σe ψ).symm w))) : S.label v ⟶ S.label w

Transport along the relabelling.

theorem MultiplicativeBasisDeformations.IndSkeleton.cv_comp {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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] {u v w : S.ARVertex} (h : S.ind (σl ψ ((σe ψ).symm u)) ⟶ S.ind (σl ψ ((σe ψ).symm v))) (h' : S.ind (σl ψ ((σe ψ).symm v)) ⟶ S.ind (σl ψ ((σe ψ).symm w))) : CategoryTheory.CategoryStruct.comp (cv ψ h) (cv ψ h') = cv ψ (CategoryTheory.CategoryStruct.comp h h')

theorem MultiplicativeBasisDeformations.IndSkeleton.cv_sub {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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] {v w : S.ARVertex} (h h' : S.ind (σl ψ ((σe ψ).symm v)) ⟶ S.ind (σl ψ ((σe ψ).symm w))) : cv ψ (h - h') = cv ψ h - cv ψ h'

theorem MultiplicativeBasisDeformations.IndSkeleton.cv_smul {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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] {v w : S.ARVertex} (t : k) (h : S.ind (σl ψ ((σe ψ).symm v)) ⟶ S.ind (σl ψ ((σe ψ).symm w))) : cv ψ (t • h) = t • cv ψ h

theorem MultiplicativeBasisDeformations.IndSkeleton.cv_sum {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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] {v w : S.ARVertex} {ι : Type u_1} (s : Finset ι) (h : ι → (S.ind (σl ψ ((σe ψ).symm v)) ⟶ S.ind (σl ψ ((σe ψ).symm w)))) : cv ψ (∑ i ∈ s, h i) = ∑ i ∈ s, cv ψ (h i)

theorem MultiplicativeBasisDeformations.IndSkeleton.cv_zero {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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] {v w : S.ARVertex} : cv ψ 0 = 0

theorem MultiplicativeBasisDeformations.IndSkeleton.mem_radPow_cv_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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] (m : ℕ) {v w : S.ARVertex} (h : S.ind (σl ψ ((σe ψ).symm v)) ⟶ S.ind (σl ψ ((σe ψ).symm w))) : cv ψ h ∈ S.radPow m (S.label v) (S.label w) ↔ h ∈ S.radPow m (S.ind (σl ψ ((σe ψ).symm v))) (S.ind (σl ψ ((σe ψ).symm w)))

theorem MultiplicativeBasisDeformations.IndSkeleton.exists_cv_Φm {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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] {v w : S.ARVertex} (h : S.label v ⟶ S.label w) : ∃ (g : S.meshObj b ((σe ψ).symm v) ⟶ S.meshObj b ((σe ψ).symm w)), cv ψ (Φm ψ S (σl ψ) (θl ψ) g) = h

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.repC {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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] {v w : S.ARVertex} (a : v ⟶ w) : S.meshObj b ((σe ψ).symm v) ⟶ S.meshObj b ((σe ψ).symm w)

The arrow representatives read in C.

theorem MultiplicativeBasisDeformations.IndSkeleton.cv_repC {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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] {v w : S.ARVertex} (a : v ⟶ w) : cv ψ (Φm ψ S (σl ψ) (θl ψ) (repC ψ a)) = S.rep b a

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.liftsC {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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] : S.Lifts b

The degree-one lifts.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.errC {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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] (x : ↑S.nonprojectiveVertices) : S.meshObj b ((σe ψ).symm ↑(S.arTranslationQuiver.tau x)) ⟶ S.meshObj b ((σe ψ).symm ↑x)

The mesh error of the degree-one lifts, read in C: homogeneous of degree two.

theorem MultiplicativeBasisDeformations.IndSkeleton.error_liftsC {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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] (x : ↑S.nonprojectiveVertices) : (liftsC ψ).error x = cv ψ (Φm ψ S (σl ψ) (θl ψ) (errC ψ x))

theorem MultiplicativeBasisDeformations.IndSkeleton.error_liftsC_eq_zero {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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] (x : ↑S.nonprojectiveVertices) : (liftsC ψ).error x = 0

The mesh errors of the degree-one lifts vanish.

theorem MultiplicativeBasisDeformations.IndSkeleton.isStandard_of_algEquiv' {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} (ψ : A ≃ₐ[k] S.A0 b) [Finite S.ARVertex] : S.IsStandard

The converse of Corollary 4.15 (cor:graded-standard-form): if A ≅ A₀, then A is standard.

theorem MultiplicativeBasisDeformations.IndSkeleton.isStandard_of_algEquiv {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) (ψ : A ≃ₐ[k] S.A0 b) : S.IsStandard

The converse of Corollary 4.15 (cor:graded-standard-form): if A ≅ A₀, then A is standard.