Multiplicative bases

MultiplicativeBasisDeformations.Foundations.ProjectiveIdempotents

Indecomposable projectives are principal right ideals eA #

Construction 2.8 keeps "the original labels P_x = e_xA" (graded-category.tex). Every indecomposable projective label is isomorphic to eA for a primitive idempotent e: a finite dual basis writes 1_P as a sum of composites P → A → P, one of them is invertible because End(P) is local, so P is a retract of A_A, and the corresponding idempotent endomorphism of A_A is left multiplication by e.

source
theorem MultiplicativeBasisDeformations.exists_isUnit_of_sum {R : Type u_1} [Ring R] [IsLocalRing R] {ι : Type u_2} (s : Finset ι) (f : ι → R) (h : IsUnit (∑ i ∈ s, f i)) :
∃ i ∈ s, IsUnit (f i)
source
theorem MultiplicativeBasisDeformations.idem_eq_zero_or_one {R : Type u_1} [Ring R] [IsLocalRing R] {p : R} (hp : IsIdempotentElem p) :
p = 0 ∨ p = 1
source
theorem MultiplicativeBasisDeformations.exists_retract_regular {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [IsLocalRing (Module.End R M)] :
∃ (u : M →ₗ[R] R) (v : R →ₗ[R] M), v ∘ₗ u = LinearMap.id

A finitely generated projective module with local endomorphism ring is a retract of the regular module.

source
theorem MultiplicativeBasisDeformations.regular_end_apply {A : Type u} [Ring A] (E : Aᵐᵒᵖ →ₗ[Aᵐᵒᵖ] Aᵐᵒᵖ) (r : Aᵐᵒᵖ) :
E r = r * E 1

An endomorphism of the regular module is right multiplication by its value at 1.

source
def MultiplicativeBasisDeformations.retractIdem {A : Type u} [Ring A] {M : Type u_1} [AddCommGroup M] [Module Aᵐᵒᵖ M] (u : M →ₗ[Aᵐᵒᵖ] Aᵐᵒᵖ) (v : Aᵐᵒᵖ →ₗ[Aᵐᵒᵖ] M) :
A

The idempotent of a retract of the regular module.

Instances For
    source
    theorem MultiplicativeBasisDeformations.u_eq_mul {A : Type u} [Ring A] {M : Type u_1} [AddCommGroup M] [Module Aᵐᵒᵖ M] (u : M →ₗ[Aᵐᵒᵖ] Aᵐᵒᵖ) (v : Aᵐᵒᵖ →ₗ[Aᵐᵒᵖ] M) (huv : v ∘ₗ u = LinearMap.id) (m : M) :
    u m = u m * (u ∘ₗ v) 1
    source
    theorem MultiplicativeBasisDeformations.unop_u_eq {A : Type u} [Ring A] {M : Type u_1} [AddCommGroup M] [Module Aᵐᵒᵖ M] (u : M →ₗ[Aᵐᵒᵖ] Aᵐᵒᵖ) (v : Aᵐᵒᵖ →ₗ[Aᵐᵒᵖ] M) (huv : v ∘ₗ u = LinearMap.id) (m : M) :
    retractIdem u v * MulOpposite.unop (u m) = MulOpposite.unop (u m)
    source
    theorem MultiplicativeBasisDeformations.retractIdem_idem {A : Type u} [Ring A] {M : Type u_1} [AddCommGroup M] [Module Aᵐᵒᵖ M] (u : M →ₗ[Aᵐᵒᵖ] Aᵐᵒᵖ) (v : Aᵐᵒᵖ →ₗ[Aᵐᵒᵖ] M) (huv : v ∘ₗ u = LinearMap.id) :
    IsIdempotentElem (retractIdem u v)
    source
    def MultiplicativeBasisDeformations.retractEquiv {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {M : Type u_1} [AddCommGroup M] [Module Aᵐᵒᵖ M] (u : M →ₗ[Aᵐᵒᵖ] Aᵐᵒᵖ) (v : Aᵐᵒᵖ →ₗ[Aᵐᵒᵖ] M) (huv : v ∘ₗ u = LinearMap.id) :
    ↥(MBDVendor.Magnitude.RightModule.rightIdeal (retractIdem u v)) ≃ₗ[Aᵐᵒᵖ] M

    eA ≅ M for a retract of the regular module.

    Instances For
      source
      theorem MultiplicativeBasisDeformations.uv_apply {A : Type u} [Ring A] {M : Type u_1} [AddCommGroup M] [Module Aᵐᵒᵖ M] (u : M →ₗ[Aᵐᵒᵖ] Aᵐᵒᵖ) (v : Aᵐᵒᵖ →ₗ[Aᵐᵒᵖ] M) (huv : v ∘ₗ u = LinearMap.id) (r : Aᵐᵒᵖ) :
      u (v r) = r * MulOpposite.op (retractIdem u v)
      source
      theorem MultiplicativeBasisDeformations.retractIdem_primitive {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {M : Type u_1} [AddCommGroup M] [Module Aᵐᵒᵖ M] (u : M →ₗ[Aᵐᵒᵖ] Aᵐᵒᵖ) (v : Aᵐᵒᵖ →ₗ[Aᵐᵒᵖ] M) (huv : v ∘ₗ u = LinearMap.id) [IsLocalRing (Module.End Aᵐᵒᵖ M)] :
      MBDVendor.Magnitude.RightModule.PrimitiveIdempotentData (retractIdem u v)

      The idempotent of a retract with local endomorphism ring is primitive.

      source
      theorem MultiplicativeBasisDeformations.IndSkeleton.exists_primitive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) (hx : CategoryTheory.Projective (S.fg x)) :
      ∃ (e : A), MBDVendor.Magnitude.RightModule.PrimitiveIdempotentData e ∧ Nonempty (MBDVendor.Magnitude.RightModule.rightIdealFGObj e ≅ S.fg x)

      Each indecomposable projective label is eA for a primitive idempotent.

      source
      theorem MultiplicativeBasisDeformations.IndSkeleton.exists_injective_label {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) (hx : CategoryTheory.Projective (S.fg x)) :
      ∃ (I : Fin S.n), ∀ (M : ModCat A), Module.finrank k (M ⟶ S.fg I) = Module.finrank k (S.fg x ⟶ M)

      The injective label of a projective label: for each indecomposable projective P_x = e_xA the indecomposable injective I_x = D(Ae_x) is a label with dim Hom_A(M, I_x) = dim Hom_A(P_x, M) (both are dim Me_x).