The Peirce isomorphism A ≅ End(⊕ e_i A)ᵒᵖ #
For a complete set of orthogonal idempotents e_i, the right ideals e_i A
with the maps between them recover A: Hom_A(e_i A, e_j A) ≅ e_j A e_i by left
multiplication, and A = ⊕ e_j A e_i. In our path-order convention for category
algebras this is an algebra isomorphism A ≅ (Alg (i ↦ e_i A))ᵒᵖ (peirceEquiv).
It is used to identify a basic algebra with the algebra A₀ of its projective
labels (Corollary 5.5, mesh-deformations.tex: "Restrict the resulting
isomorphism ind(mod A) ≅ C to the labelled projective objects and take
opposite algebras").
@[reducible, inline]
The right ideal e_i A as a right module.
Instances For
def
MultiplicativeBasisDeformations.lmul
{A : Type u}
[Ring A]
{a b : A}
(hb : IsIdempotentElem b)
(y : A)
(hy : b * y = y)
:
Left multiplication by y ∈ e_j A as a map e_i A → e_j A.
Instances For
theorem
MultiplicativeBasisDeformations.lmul_apply
{A : Type u}
[Ring A]
{a b : A}
(hb : IsIdempotentElem b)
(y : A)
(hy : b * y = y)
(m : ↥(MBDVendor.Magnitude.RightModule.rightIdeal a))
:
↑((lmul hb y hy) m) = y * ↑m
theorem
MultiplicativeBasisDeformations.e_mul_corner
{A : Type u}
[Ring A]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{e : ι → A}
(he : CompleteOrthogonalIdempotents e)
(i j : ι)
(x : A)
:
e j * (e j * x * e i) = e j * x * e i
def
MultiplicativeBasisDeformations.peirceFun
{A : Type u}
[Ring A]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{e : ι → A}
(he : CompleteOrthogonalIdempotents e)
(x : A)
:
(CatAlg.Alg fun (i : ι) => idealMod (e i))ᵐᵒᵖ
The Peirce map x ↦ (left multiplication by e_j x e_i).
Instances For
theorem
MultiplicativeBasisDeformations.peirceFun_apply
{A : Type u}
[Ring A]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{e : ι → A}
(he : CompleteOrthogonalIdempotents e)
(x : A)
(i j : ι)
(m : ↥(MBDVendor.Magnitude.RightModule.rightIdeal (e i)))
:
↑((ModuleCat.Hom.hom (MulOpposite.unop (peirceFun he x) i j)) m) = e j * x * e i * ↑m
theorem
MultiplicativeBasisDeformations.peirce_ext
{A : Type u}
[Ring A]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{e : ι → A}
{a b : (CatAlg.Alg fun (i : ι) => idealMod (e i))ᵐᵒᵖ}
(h :
∀ (i j : ι) (m : ↥(MBDVendor.Magnitude.RightModule.rightIdeal (e i))),
↑((ModuleCat.Hom.hom (MulOpposite.unop a i j)) m) = ↑((ModuleCat.Hom.hom (MulOpposite.unop b i j)) m))
:
a = b
Entrywise extensionality for elements of (Alg P)ᵒᵖ.
theorem
MultiplicativeBasisDeformations.ideal_fixed
{A : Type u}
[Ring A]
{a : A}
(ha : IsIdempotentElem a)
(m : ↥(MBDVendor.Magnitude.RightModule.rightIdeal a))
:
a * ↑m = ↑m
theorem
MultiplicativeBasisDeformations.idTo_apply
{A : Type u}
[Ring A]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{e : ι → A}
(he : CompleteOrthogonalIdempotents e)
(i j : ι)
(m : ↥(MBDVendor.Magnitude.RightModule.rightIdeal (e i)))
:
↑((ModuleCat.Hom.hom (CatAlg.idTo i j)) m) = e j * e i * ↑m
theorem
MultiplicativeBasisDeformations.sum_corner
{A : Type u}
[Ring A]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{e : ι → A}
(he : CompleteOrthogonalIdempotents e)
(x : A)
:
x = ∑ i : ι, ∑ j : ι, e j * x * e i
theorem
MultiplicativeBasisDeformations.smul_alg_apply
{k : Type u}
[Field k]
{A : Type u}
[Ring A]
[Algebra k A]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{e : ι → A}
(c : k)
(a : CatAlg.Alg fun (i : ι) => idealMod (e i))
(i j : ι)
(m : ↥(MBDVendor.Magnitude.RightModule.rightIdeal (e i)))
:
↑((ModuleCat.Hom.hom ((c • a) i j)) m) = ↑((ModuleCat.Hom.hom (a i j)) m) * (algebraMap k A) c
def
MultiplicativeBasisDeformations.peirceHom
{k : Type u}
[Field k]
{A : Type u}
[Ring A]
[Algebra k A]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{e : ι → A}
(he : CompleteOrthogonalIdempotents e)
:
A →ₐ[k] (CatAlg.Alg fun (i : ι) => idealMod (e i))ᵐᵒᵖ
The Peirce algebra homomorphism.
Instances For
def
MultiplicativeBasisDeformations.gen
{A : Type u}
[Ring A]
{ι : Type}
[Fintype ι]
{e : ι → A}
(he : CompleteOrthogonalIdempotents e)
(i : ι)
:
The generator e_i of e_i A.
Instances For
noncomputable def
MultiplicativeBasisDeformations.peirceEquiv
{k : Type u}
[Field k]
{A : Type u}
[Ring A]
[Algebra k A]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{e : ι → A}
(he : CompleteOrthogonalIdempotents e)
:
A ≃ₐ[k] (CatAlg.Alg fun (i : ι) => idealMod (e i))ᵐᵒᵖ
The Peirce isomorphism A ≅ (Alg (i ↦ e_i A))ᵒᵖ.
Instances For
Category algebras along fully faithful functors #
def
MultiplicativeBasisDeformations.CatAlg.mapAlg
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
{ι : Type}
{F : ι → C}
{G : ι → D}
(Φ : CategoryTheory.Functor C D)
(α : (i : ι) → Φ.obj (F i) ≅ G i)
(a : Alg F)
:
Alg G
The transport of a matrix along Φ and α.
Instances For
noncomputable def
MultiplicativeBasisDeformations.CatAlg.unmapAlg
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
{ι : Type}
{F : ι → C}
{G : ι → D}
(Φ : CategoryTheory.Functor C D)
[Φ.Full]
(α : (i : ι) → Φ.obj (F i) ≅ G i)
(b : Alg G)
:
Alg F
And back.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.mapAlg_one
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Preadditive D]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → C}
{G : ι → D}
(Φ : CategoryTheory.Functor C D)
[Φ.Full]
[Φ.Faithful]
[Φ.Additive]
(α : (i : ι) → Φ.obj (F i) ≅ G i)
:
mapAlg Φ α 1 = 1
theorem
MultiplicativeBasisDeformations.CatAlg.mapAlg_mul
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Preadditive D]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → C}
{G : ι → D}
(Φ : CategoryTheory.Functor C D)
[Φ.Full]
[Φ.Faithful]
[Φ.Additive]
(α : (i : ι) → Φ.obj (F i) ≅ G i)
(a b : Alg F)
:
theorem
MultiplicativeBasisDeformations.CatAlg.mapAlg_add
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Preadditive D]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → C}
{G : ι → D}
(Φ : CategoryTheory.Functor C D)
[Φ.Full]
[Φ.Faithful]
[Φ.Additive]
(α : (i : ι) → Φ.obj (F i) ≅ G i)
(a b : Alg F)
:
theorem
MultiplicativeBasisDeformations.CatAlg.mapAlg_smul
{k : Type u₁}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k D]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → C}
{G : ι → D}
(Φ : CategoryTheory.Functor C D)
[Φ.Full]
[Φ.Faithful]
[Φ.Additive]
[CategoryTheory.Functor.Linear k Φ]
(α : (i : ι) → Φ.obj (F i) ≅ G i)
(c : k)
(a : Alg F)
:
noncomputable def
MultiplicativeBasisDeformations.CatAlg.algEquivOfFunctor
{k : Type u₁}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k D]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → C}
{G : ι → D}
(Φ : CategoryTheory.Functor C D)
[Φ.Full]
[Φ.Faithful]
[Φ.Additive]
[CategoryTheory.Functor.Linear k Φ]
(α : (i : ι) → Φ.obj (F i) ≅ G i)
:
Category algebras along a fully faithful linear functor.