Coordinate-thin consequences for local modules #
Small reusable consequences of the global all-indecomposables-coordinate-thin hypothesis for finitely generated modules with simple top.
theorem
MagnitudeConjecture.RightModule.coordinateThin_of_simpleTop
{k A : Type u}
{ι : Type w}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(e : ι → A)
(H : AllIndecomposablesCoordinateThin e)
(W : FinitelyGeneratedCategory A)
(htop : IsSimpleModule Aᵐᵒᵖ (↑W ⧸ Module.jacobson Aᵐᵒᵖ ↑W))
:
IsCoordinateThin e W
A finitely generated module with simple top is one of the indecomposables controlled by the all-coordinate-thin premise.
theorem
MagnitudeConjecture.RightModule.nonisomorphic_top_and_nonzero_jacobson_submodule_of_simpleTop
{k A : Type u}
{ι : Type w}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[Fintype ι]
(e : ι → A)
(hall : CompleteOrthogonalIdempotents e)
(H : AllIndecomposablesCoordinateThin e)
(W : FinitelyGeneratedCategory A)
(htop : IsSimpleModule Aᵐᵒᵖ (↑W ⧸ Module.jacobson Aᵐᵒᵖ ↑W))
(P : Submodule Aᵐᵒᵖ ↑W)
(hPne : P ≠ ⊥)
(hPJ : P ≤ Module.jacobson Aᵐᵒᵖ ↑W)
:
¬Nonempty ((↑W ⧸ Module.jacobson Aᵐᵒᵖ ↑W) ≃ₗ[Aᵐᵒᵖ] ↥P)
Under the global coordinate-thin premise, the simple top of a local module is nonisomorphic to every nonzero submodule of its radical.
theorem
MagnitudeConjecture.RightModule.no_repeatedSelfSubquotient_of_simpleTop_of_all_coordinateThin
{k A : Type u}
{ι : Type w}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[Fintype ι]
(e : ι → A)
(hall : CompleteOrthogonalIdempotents e)
(H : AllIndecomposablesCoordinateThin e)
(W : FinitelyGeneratedCategory A)
(htop : IsSimpleModule Aᵐᵒᵖ (↑W ⧸ Module.jacobson Aᵐᵒᵖ ↑W))
:
Under a complete coordinate family, a simple-top module cannot contain the repeated self-subquotient used by any obstruction construction.
theorem
MagnitudeConjecture.RightModule.nonisomorphic_disjoint_simple_submodules_of_simpleTop
{k A : Type u}
{ι : Type w}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[Fintype ι]
(e : ι → A)
(hall : CompleteOrthogonalIdempotents e)
(H : AllIndecomposablesCoordinateThin e)
(W : FinitelyGeneratedCategory A)
(htop : IsSimpleModule Aᵐᵒᵖ (↑W ⧸ Module.jacobson Aᵐᵒᵖ ↑W))
(P Q : Submodule Aᵐᵒᵖ ↑W)
(hP : IsSimpleModule Aᵐᵒᵖ ↥P)
(hinf : P ⊓ Q = ⊥)
:
¬Nonempty (↥P ≃ₗ[Aᵐᵒᵖ] ↥Q)
Two disjoint simple submodules of a coordinate-thin local module are nonisomorphic.