Almost-splitness and minimality under natural isomorphism #
theorem
MagnitudeConjecture.CategoryTheory.rightAlmostSplit_map_of_natIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
{F G : CategoryTheory.Functor C D}
(e : F ≅ G)
{X Y : C}
(f : X ⟶ Y)
(hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (G.map f))
:
Isomorphic realizations have the same right almost-split maps.
theorem
MagnitudeConjecture.CategoryTheory.rightMinimal_map_of_natIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
{F G : CategoryTheory.Functor C D}
(e : F ≅ G)
[CategoryTheory.Preadditive D]
{X Y : C}
(f : X ⟶ Y)
(hf : QuotientSubmoduleEquidistribution.IsRightMinimal (G.map f))
:
Isomorphic realizations have the same right-minimal maps.