Endpoint-stable Hom subspaces #
This file isolates the local categorical language used in the Jans--Kupisch argument. A Hom subspace is a subbimodule when it is stable under precomposition and postcomposition by endpoint endomorphisms.
def
MagnitudeConjecture.IsHomSubbimodule
{k : Type w}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{X Y : C}
(S : Submodule k (X ⟶ Y))
:
A linear subspace of one Hom space stable under both endpoint endomorphism rings.
Instances For
def
MagnitudeConjecture.twoSidedEndomorphismSpan
{k : Type w}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{X Y : C}
(f : X ⟶ Y)
:
Submodule k (X ⟶ Y)
The linear span of all two-sided endpoint multiples of one morphism.
Instances For
theorem
MagnitudeConjecture.isHomSubbimodule_twoSidedEndomorphismSpan
{k : Type w}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{X Y : C}
(f : X ⟶ Y)
:
A principal two-sided endomorphism span is endpoint-stable.
theorem
MagnitudeConjecture.mem_twoSidedEndomorphismSpan
{k : Type w}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{X Y : C}
(f : X ⟶ Y)
:
f ∈ twoSidedEndomorphismSpan f
The generator belongs to its principal two-sided span.
theorem
MagnitudeConjecture.twoSidedEndomorphismSpan_le_of_mem
{k : Type w}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{X Y : C}
{f g : X ⟶ Y}
(hg : g ∈ twoSidedEndomorphismSpan f)
:
Membership in a principal two-sided span implies inclusion of principal spans.
def
MagnitudeConjecture.AllowsTransit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
:
Every source endomorphism can be transferred across a morphism to its target endpoint.
Instances For
def
MagnitudeConjecture.AllowsCotransit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
:
Every target endomorphism can be transferred across a morphism to its source endpoint.