Almost-split morphisms under equivalence

An ordinary categorical equivalence preserves right and left almost-split morphisms and their minimality. The proof uses essential surjectivity to pull an arbitrary test object back across the equivalence and full faithfulness to reflect splittings.

This is the covariant companion of the anti-equivalence argument in QuotientSubmoduleEquidistribution.RepresentationTheory.AlmostSplitDuality; only the two transport lemmas required by the support-algebra passage are included here.

theorem QuotientSubmoduleEquidistribution.IsRightAlmostSplit.map_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {X Y : C} {f : X ⟶ Y} (hf : IsRightAlmostSplit f) (E : C ≌ D) : IsRightAlmostSplit (E.functor.map f)

A right almost-split morphism remains right almost split after applying an equivalence.

theorem QuotientSubmoduleEquidistribution.IsRightAlmostSplit.of_map_fully_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] {X Y : C} {f : X ⟶ Y} (hf : IsRightAlmostSplit (F.map f)) : IsRightAlmostSplit f

Right almost-splitness is reflected by a fully faithful functor.

theorem QuotientSubmoduleEquidistribution.IsRightAlmostSplit.of_map_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {X Y : C} {f : X ⟶ Y} (E : C ≌ D) (hf : IsRightAlmostSplit (E.functor.map f)) : IsRightAlmostSplit f

Right almost-splitness is reflected by an equivalence.

theorem QuotientSubmoduleEquidistribution.IsLeftAlmostSplit.map_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {X Y : C} {f : X ⟶ Y} (hf : IsLeftAlmostSplit f) (E : C ≌ D) : IsLeftAlmostSplit (E.functor.map f)

A left almost-split morphism remains left almost split after applying an equivalence.

theorem QuotientSubmoduleEquidistribution.IsLeftAlmostSplit.of_map_fully_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] {X Y : C} {f : X ⟶ Y} (hf : IsLeftAlmostSplit (F.map f)) : IsLeftAlmostSplit f

Left almost-splitness is reflected by a fully faithful functor.

theorem QuotientSubmoduleEquidistribution.IsLeftAlmostSplit.of_map_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {X Y : C} {f : X ⟶ Y} (E : C ≌ D) (hf : IsLeftAlmostSplit (E.functor.map f)) : IsLeftAlmostSplit f

Left almost-splitness is reflected by an equivalence.

theorem QuotientSubmoduleEquidistribution.IsLeftAlmostSplit.postcomp_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Y' : C} {f : X ⟶ Y} (hf : IsLeftAlmostSplit f) (e : Y ≅ Y') : IsLeftAlmostSplit (CategoryTheory.CategoryStruct.comp f e.hom)

Postcomposition by an isomorphism preserves left almost-splitness.

theorem QuotientSubmoduleEquidistribution.IsRightMinimal.map_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {X Y : C} {f : X ⟶ Y} (hf : IsRightMinimal f) (E : C ≌ D) : IsRightMinimal (E.functor.map f)

Right minimality is preserved after applying an equivalence.

theorem QuotientSubmoduleEquidistribution.IsLeftMinimal.map_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {X Y : C} {f : X ⟶ Y} (hf : IsLeftMinimal f) (E : C ≌ D) : IsLeftMinimal (E.functor.map f)

Left minimality is preserved after applying an equivalence.