A standard basic algebra is its projective algebra A₀

Corollary 5.5 (mesh-deformations.tex): "Restrict the resulting isomorphism ind(mod A) ≅ C to the labelled projective objects and take opposite algebras. Construction 2.8 and Proposition 4.14 give A ≅ A₀ ≅ kP."

For a basic algebra with idempotents e_i, the projective vertices of Γ_A correspond to the e_i (pvEquiv, with S.obj p ≅ e_{σ p} A). A standard equivalence k(Γ_A) ≃ ind(mod A) then gives A₀ = (Alg F₀)ᵒᵖ ≅ (Alg (e_{σ p} A))ᵒᵖ ≅ A (algEquivA0, with the Peirce isomorphism).

theorem MultiplicativeBasisDeformations.IndSkeleton.isPrimitive_of_data {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {a : A} (D : MBDVendor.Magnitude.RightModule.PrimitiveIdempotentData a) : IsPrimitiveIdempotent a

theorem MultiplicativeBasisDeformations.IndSkeleton.data_of_isPrimitive {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {a : A} (h : IsPrimitiveIdempotent a) : MBDVendor.Magnitude.RightModule.PrimitiveIdempotentData a

def MultiplicativeBasisDeformations.IndSkeleton.isoObj {A : Type u} [Ring A] {M N : ModCat A} (φ : M ≅ N) : M.obj ≅ N.obj

An isomorphism of finitely generated modules as an isomorphism of modules.

theorem MultiplicativeBasisDeformations.IndSkeleton.exists_iso_label {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)) (p : (S.arMeshData b).PV) : ∃ (i : Fin n), Nonempty (S.obj (S.index ↑p) ≅ idealMod (e i))

Each projective label is some e_i A.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.σv {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)) (p : (S.arMeshData b).PV) : Fin n

The idempotent of a projective vertex.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.isoLabel {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)) (p : (S.arMeshData b).PV) : S.obj (S.index ↑p) ≅ idealMod (e (S.σv b he hprim p))

S.obj p ≅ e_{σ p} A.

theorem MultiplicativeBasisDeformations.IndSkeleton.σv_injective {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)) : Function.Injective (S.σv b he hprim)

theorem MultiplicativeBasisDeformations.IndSkeleton.σv_surjective {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) : Function.Surjective (S.σv b he hprim)

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.pvEquiv {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) : (S.arMeshData b).PV ≃ Fin n

Projective vertices ↔ idempotents.

theorem MultiplicativeBasisDeformations.IndSkeleton.pvEquiv_apply {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) (p : (S.arMeshData b).PV) : (S.pvEquiv b he hprim hbasic) p = S.σv b he hprim p

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.algEquivA0 {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) (Φ0 : CategoryTheory.Functor (S.ARMeshCategory b) S.Ind) [Φ0.IsEquivalence] (hlin : IsLinearFunctor Φ0) (β : (x : S.ARVertex) → Φ0.obj (S.meshObj b x) ≅ S.label x) : A ≃ₐ[k] (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ

A ≅ A₀ for a basic algebra with a standard equivalence.

theorem MultiplicativeBasisDeformations.IndSkeleton.hasNormedBasis_of_subsingleton {k A : Type u} [Field k] [Ring A] [Algebra k A] [Subsingleton A] : HasNormedMultiplicativeBasis k A

A trivial algebra has a normed multiplicative basis (the empty one).

theorem MultiplicativeBasisDeformations.IndSkeleton.hasNormedBasis_of_isStandard {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) {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) (hstd : S.IsStandard) : HasNormedMultiplicativeBasis k A

A standard basic algebra has a normed multiplicative basis (Corollary 5.5(2)): A ≅ A₀ and A₀ has one (Proposition 4.14).