Independent families and the skeletons of the proof library #
An independent complete family of indecomposable right modules is an
IndSkeleton of the proof library with the same objects. The radical powers,
the spaces of irreducible maps and the Auslander–Reiten quivers agree.
def
MultiplicativeBasisDeformations.Statement.toSkeleton
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
(S : IndecomposableFamily k A)
:
IndSkeleton k A
The family as a skeleton of the proof library.
Instances For
theorem
MultiplicativeBasisDeformations.Statement.radPow_eq
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
(S : IndecomposableFamily k A)
(n : ℕ)
(X Y : Ind S)
:
radPow S n X Y = (toSkeleton S).radPow n X Y
theorem
MultiplicativeBasisDeformations.Statement.finrank_irr_eq
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
(S : IndecomposableFamily k A)
(X Y : Ind S)
:
Module.finrank k (Irr S X Y) = Module.finrank k ((toSkeleton S).Irr X Y)