Indecomposable projectives of a basic algebra

For Corollary 5.5 (mesh-deformations.tex) we identify a basic algebra A with the algebra A₀ of its projective labels. Here: the right ideal eA of a primitive idempotent is isomorphic to e_i A for one idempotent of a complete set (exists_iso_ideal: some e e_i e is a unit of the local corner eAe, so eA is a retract of e_i A), and for a basic algebra distinct e_i A are not isomorphic (eq_of_iso_ideal).

The corner ring of a primitive idempotent is local

theorem MultiplicativeBasisDeformations.corner_isLocalRing_of_primitive (k : Type u) [Field k] {R : Type u_1} [Ring R] [Algebra k R] [FiniteDimensional k R] {e : R} (hp : IsPrimitiveIdempotent e) : IsLocalRing ⋯.Corner

Endomorphisms of eA

def MultiplicativeBasisDeformations.genOf {A : Type u} [Ring A] {a : A} (ha : IsIdempotentElem a) : ↥(MBDVendor.Magnitude.RightModule.rightIdeal a)

The generator of eA.

theorem MultiplicativeBasisDeformations.hom_gen_val {A : Type u} [Ring A] {a b : A} (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) (f : idealMod a ⟶ idealMod b) : b * ↑((ModuleCat.Hom.hom f) (genOf ha)) * a = ↑((ModuleCat.Hom.hom f) (genOf ha))

theorem MultiplicativeBasisDeformations.hom_apply_eq {A : Type u} [Ring A] {a b : A} (ha : IsIdempotentElem a) (f : idealMod a ⟶ idealMod b) (m : ↥(MBDVendor.Magnitude.RightModule.rightIdeal a)) : ↑((ModuleCat.Hom.hom f) m) = ↑((ModuleCat.Hom.hom f) (genOf ha)) * ↑m

def MultiplicativeBasisDeformations.endEquivCorner {A : Type u} [Ring A] {a : A} (ha : IsIdempotentElem a) : CategoryTheory.End (idealMod a) ≃+* ha.Corner

End(eA) ≅ eAe.

theorem MultiplicativeBasisDeformations.idealMod_end_isLocalRing (k : Type u) [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] {a : A} (hp : IsPrimitiveIdempotent a) : IsLocalRing (CategoryTheory.End (idealMod a))

theorem MultiplicativeBasisDeformations.idealMod_not_isZero {A : Type u} [Ring A] {a : A} (hp : IsPrimitiveIdempotent a) : ¬CategoryTheory.Limits.IsZero (idealMod a)

eA ≅ e_i A

theorem MultiplicativeBasisDeformations.cornerVal_sum {A : Type u} [Ring A] {a : A} (ha : IsIdempotentElem a) {ι : Type u_1} (s : Finset ι) (f : ι → ha.Corner) : cornerVal ha (∑ i ∈ s, f i) = ∑ i ∈ s, cornerVal ha (f i)

theorem MultiplicativeBasisDeformations.exists_iso_ideal (k : Type u) [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] {e : A} (hp : IsPrimitiveIdempotent e) {ι : Type u_1} [Fintype ι] {e' : ι → A} (he' : CompleteOrthogonalIdempotents e') (hp' : ∀ (i : ι), IsPrimitiveIdempotent (e' i)) : ∃ (i : ι), Nonempty (idealMod e ≅ idealMod (e' i))

The right ideal of a primitive idempotent is one of the e_i A.

theorem MultiplicativeBasisDeformations.basic_data_of_iso {A : Type u} [Ring A] {a b : A} (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) (φ : idealMod a ≅ idealMod b) : ∃ (x : A) (y : A), a * x * b = x ∧ b * y * a = y ∧ x * y = a ∧ y * x = b

Isomorphic e_i A, e_j A give the data of the basic condition.