Uniserial ideals generated by ordinary arrows #
The preliminary Skowroński--Waschbüsch lemma starts from a biserial
primitive-projective presentation and Kupisch condition (K)(2). This file
derives the missing structural input: every representative of an ordinary
arrow generates a uniserial principal right ideal, and dually a uniserial
principal left ideal.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.boundaryRadicalTop_isCoordinateThin_of_uniserialAlternative
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(P : S.PrimitiveProjectivePresentation)
(D : OrdinaryArrowRepresentatives)
(hHomAlternative :
∀ (x y : S.ProjectiveLabel),
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj x))
(S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x) ∨ IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj y))ᵐᵒᵖ
(S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x))
(x : S.ProjectiveLabel)
:
Kupisch condition (K)(2) makes the first radical layer of every
selected projective coordinate-thin.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomRangePrincipalRightIdealLinearEquiv
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(P : S.PrimitiveProjectivePresentation)
{p q : S.ProjectiveLabel}
(f : S.ordinaryProjectiveObj p ⟶ S.ordinaryProjectiveObj q)
:
↥(ModuleCat.Hom.hom (P.projectiveHomTransport f).hom).range ≃ₗ[Aᵐᵒᵖ] ↥(rightIdeal (P.projectiveHomCoordinate f))
The image of a selected-projective morphism, after transport to literal principal projectives, is canonically the principal right ideal generated by its algebra coordinate.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_radicalSquare_lift_with_uniserial_range_of_radical
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(P : S.PrimitiveProjectivePresentation)
(hP : P.IsBiserial)
(D : OrdinaryArrowRepresentatives)
(hHomAlternative :
∀ (x y : S.ProjectiveLabel),
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj x))
(S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x) ∨ IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj y))ᵐᵒᵖ
(S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x))
{x y : S.ProjectiveLabel}
(f : ↥(S.projectiveRadicalSubmodule x y))
:
∃ (b : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x),
IsUniserialModule Aᵐᵒᵖ ↥(ModuleCat.Hom.hom (S.ordinaryProjectiveFGHom b).hom).range ∧ b - ↑f ∈ S.projectiveRadicalSquareSubmodule x y
A radical morphism can be changed only by an internal radical-square morphism so that its image lies in one uniserial branch of the target projective radical.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_radicalSquare_lift_with_uniserial_range
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(P : S.PrimitiveProjectivePresentation)
(hP : P.IsBiserial)
(D : OrdinaryArrowRepresentatives)
(hHomAlternative :
∀ (x y : S.ProjectiveLabel),
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj x))
(S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x) ∨ IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj y))ᵐᵒᵖ
(S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x))
{x y : S.ProjectiveLabel}
(a : S.OrdinaryArrow x y)
:
∃ (b : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x),
IsUniserialModule Aᵐᵒᵖ ↥(ModuleCat.Hom.hom (S.ordinaryProjectiveFGHom b).hom).range ∧ b - D.hom a ∈ S.projectiveRadicalSquareSubmodule x y
The radical lift specialized to a displayed ordinary-arrow representative.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.codomainEndomorphism_mem_radical_of_nonSquare
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{x y : S.ProjectiveLabel}
(f : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x)
(hf : f ∉ S.projectiveRadicalSquareSubmodule x y)
(e : S.ordinaryProjectiveObj x ⟶ S.ordinaryProjectiveObj x)
(hcomp : CategoryTheory.CategoryStruct.comp f e ∈ S.projectiveRadicalSquareSubmodule x y)
:
e ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj x) (S.ordinaryProjectiveObj x)
A postcomposition multiplier carrying a radical morphism which survives modulo the radical square into the square is itself radical.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.domainEndomorphism_mem_radical_of_nonSquare
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{x y : S.ProjectiveLabel}
(f : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x)
(hf : f ∉ S.projectiveRadicalSquareSubmodule x y)
(e : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj y)
(hcomp : CategoryTheory.CategoryStruct.comp e f ∈ S.projectiveRadicalSquareSubmodule x y)
:
e ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj y) (S.ordinaryProjectiveObj y)
The precomposition analogue of
codomainEndomorphism_mem_radical_of_nonSquare.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.radical_range_isUniserial_of_not_mem_square
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(P : S.PrimitiveProjectivePresentation)
(hP : P.IsBiserial)
(D : OrdinaryArrowRepresentatives)
(hHomAlternative :
∀ (x y : S.ProjectiveLabel),
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj x))
(S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x) ∨ IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj y))ᵐᵒᵖ
(S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x))
{x y : S.ProjectiveLabel}
(f : ↥(S.projectiveRadicalSubmodule x y))
(hf : ↑f ∉ S.projectiveRadicalSquareSubmodule x y)
:
IsUniserialModule Aᵐᵒᵖ ↥(ModuleCat.Hom.hom (S.ordinaryProjectiveFGHom ↑f).hom).range
The radical-square branch lift and Kupisch (K)(2) imply that every
radical morphism which survives modulo the radical square has uniserial
image. The endpoint multiplier relating it to the branch lift differs from
the identity by a nilpotent radical endomorphism and is therefore invertible.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.ordinaryArrow_range_isUniserial
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(P : S.PrimitiveProjectivePresentation)
(hP : P.IsBiserial)
(D : OrdinaryArrowRepresentatives)
(hHomAlternative :
∀ (x y : S.ProjectiveLabel),
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj x))
(S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x) ∨ IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj y))ᵐᵒᵖ
(S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x))
{x y : S.ProjectiveLabel}
(a : S.OrdinaryArrow x y)
:
IsUniserialModule Aᵐᵒᵖ ↥(ModuleCat.Hom.hom (S.ordinaryProjectiveFGHom (D.hom a)).hom).range
Every displayed ordinary-arrow representative has uniserial image.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.radical_rightIdeal_isUniserial_of_not_mem_square
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(P : S.PrimitiveProjectivePresentation)
(hP : P.IsBiserial)
(D : OrdinaryArrowRepresentatives)
(hHomAlternative :
∀ (x y : S.ProjectiveLabel),
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj x))
(S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x) ∨ IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj y))ᵐᵒᵖ
(S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x))
{x y : S.ProjectiveLabel}
(f : ↥(S.projectiveRadicalSubmodule x y))
(hf : ↑f ∉ S.projectiveRadicalSquareSubmodule x y)
:
IsUniserialModule Aᵐᵒᵖ ↥(rightIdeal (P.projectiveHomCoordinate ↑f))
Every radical morphism which survives modulo the radical square generates a uniserial principal right ideal.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.ordinaryArrow_rightIdeal_isUniserial
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(P : S.PrimitiveProjectivePresentation)
(hP : P.IsBiserial)
(D : OrdinaryArrowRepresentatives)
(hHomAlternative :
∀ (x y : S.ProjectiveLabel),
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj x))
(S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x) ∨ IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj y))ᵐᵒᵖ
(S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x))
{x y : S.ProjectiveLabel}
(a : S.OrdinaryArrow x y)
:
IsUniserialModule Aᵐᵒᵖ ↥(rightIdeal (P.projectiveHomCoordinate (D.hom a)))
Every displayed ordinary-arrow representative generates a uniserial principal right ideal.
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositePresentation_idempotent_oppositeProjectiveCoordinate
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ]
(P : S.PrimitiveProjectivePresentation)
(p : S.ProjectiveLabel)
:
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositePresentation_primitiveProjectiveIso_coordinate
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ]
(P : S.PrimitiveProjectivePresentation)
(p : S.ProjectiveLabel)
:
P.oppositePresentation.primitiveProjectiveIso (P.oppositeProjectiveCoordinate p) = CategoryTheory.eqToIso ⋯ ≪≫ P.oppositeProjectiveCoordinateIso p
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.opposite_projectiveRadical_coordinate
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ]
(P : S.PrimitiveProjectivePresentation)
{p q : S.ProjectiveLabel}
(f : ↥(S.projectiveRadicalSubmodule p q))
:
P.oppositePresentation.projectiveHomCoordinate ↑((P.projectiveRadicalOppositeLinearEquiv p q) f) = MulOpposite.op (P.projectiveHomCoordinate ↑f)
The opposite-presentation coordinate of a dualized projective radical morphism is the opposite of its original algebra coordinate.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.ordinaryArrow_leftIdeal_isUniserial
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(P : S.PrimitiveProjectivePresentation)
(hP : P.IsBiserial)
(D : OrdinaryArrowRepresentatives)
{x y : S.ProjectiveLabel}
(a : S.OrdinaryArrow x y)
:
IsUniserialModule A ↥(leftIdeal (P.projectiveHomCoordinate (D.hom a)))
Every displayed ordinary-arrow representative generates a uniserial principal left ideal.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_adapted_of_isBiserial
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(P : S.PrimitiveProjectivePresentation)
(hP : P.IsBiserial)
:
A representation-finite biserial primitive presentation admits ordinary arrow representatives satisfying both special-biserial continuation bounds.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.admitsSpecialBiserialPresentation_of_isBiserial
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(P : S.PrimitiveProjectivePresentation)
(hP : P.IsBiserial)
:
A representation-finite biserial basic algebra has a literal special-biserial bound-quiver presentation.