Almost-split morphisms under anti-equivalence

An equivalence from an opposite category turns a minimal right almost-split morphism into a minimal left almost-split morphism. The small generic proof is adapted from the adjacent OP-conjecture formalization; no OP-specific theorem or module is imported.

theorem QuotientSubmoduleEquidistribution.IsLeftAlmostSplit.op {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (hf : IsLeftAlmostSplit f) : IsRightAlmostSplit f.op

A left almost-split morphism becomes right almost split after passage to the opposite category.

theorem QuotientSubmoduleEquidistribution.IsRightAlmostSplit.map_op_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) : IsLeftAlmostSplit (E.functor.map f.op)

A right almost-split morphism becomes left almost split under an anti-equivalence.

theorem QuotientSubmoduleEquidistribution.IsRightMinimal.map_op_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) : IsLeftMinimal (E.functor.map f.op)

A right-minimal morphism becomes left minimal under an anti-equivalence.

Irreducible morphisms

theorem QuotientSubmoduleEquidistribution.IsIrreducibleMorphism.op {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (hf : IsIrreducibleMorphism f) : IsIrreducibleMorphism f.op

Opposite-category passage preserves irreducibility and reverses the direction of the morphism.

theorem QuotientSubmoduleEquidistribution.IsIrreducibleMorphism.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 : IsIrreducibleMorphism f) (E : C ≌ D) : IsIrreducibleMorphism (E.functor.map f)

A categorical equivalence preserves irreducible morphisms.

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

Precomposition by an isomorphism preserves irreducibility.

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

Postcomposition by an isomorphism preserves irreducibility.

noncomputable def QuotientSubmoduleEquidistribution.cokernelMapOpIsoKernel {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (E : Cᵒᵖ ≌ D) {X Y : C} (f : X ⟶ Y) : CategoryTheory.Limits.cokernel (E.functor.map f.op) ≅ E.functor.obj (Opposite.op (CategoryTheory.Limits.kernel f))

The cokernel of the contravariant image of a morphism is canonically isomorphic to the image of its kernel.

noncomputable def QuotientSubmoduleEquidistribution.cokernelPrecompMapOpIsoKernel {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (E : Cᵒᵖ ≌ D) {X Y : C} (f : X ⟶ Y) {Y' : D} (i : Y' ≅ E.functor.obj (Opposite.op Y)) : CategoryTheory.Limits.cokernel (CategoryTheory.CategoryStruct.comp i.hom (E.functor.map f.op)) ≅ E.functor.obj (Opposite.op (CategoryTheory.Limits.kernel f))

Precomposing the mapped morphism by an endpoint isomorphism does not change its cokernel.