Irreducible morphisms under locally closed functors

A fully faithful functor always reflects irreducible morphisms, but need not preserve them: an image morphism might acquire a factorization through an object outside the essential image. For one fixed morphism, preservation only requires the intermediate objects of factorizations whose two factors are nonsplit to lie in the essential image. This is the precise categorical role of the manuscript's third Hom-neighborhood in the covering argument.

def MagnitudeConjecture.IsLocallyFactorizationClosedAt {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) : Prop

The essential image of F contains every intermediate object needed to test irreducibility of F.map f. Factorizations already split on one side need no lifting and are omitted from the condition.

theorem MagnitudeConjecture.irreducible_of_map_of_full_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 : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (F.map f)) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f

Full faithfulness reflects irreducibility without any hypothesis on objects outside the image.

theorem MagnitudeConjecture.irreducible_map_of_full_faithful_of_locallyFactorizationClosed {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 : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f) (hclosed : IsLocallyFactorizationClosedAt F f) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (F.map f)

A fully faithful functor preserves irreducibility at a morphism when all new nonsplit factorizations have intermediate object in its essential image.

theorem MagnitudeConjecture.isIrreducibleMorphism_map_iff_of_locallyFactorizationClosed {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} (hclosed : IsLocallyFactorizationClosedAt F f) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (F.map f) ↔ QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f

Under local factorization closure, full faithfulness identifies irreducibility on the nose.