Subobject orders under categorical equivalence

A fully faithful functor embeds the subobject order of an object into the subobject order of its image. For an equivalence this embedding is surjective, hence an order isomorphism.

noncomputable def MagnitudeConjecture.CategoryTheory.subobjectOrderEmbedding {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] [F.PreservesMonomorphisms] (X : C) : CategoryTheory.Subobject X ↪o CategoryTheory.Subobject (F.obj X)

A fully faithful mono-preserving functor embeds the subobject order of an object into the subobject order of its image.

noncomputable def MagnitudeConjecture.CategoryTheory.fullSubcategorySubobjectOrderIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderSubobjects] (X : P.FullSubcategory) : CategoryTheory.Subobject X ≃o CategoryTheory.Subobject X.obj

If an object property is closed under subobjects, passing from its full subcategory to the ambient category does not change the subobject order.

noncomputable def MagnitudeConjecture.CategoryTheory.Equivalence.subobjectOrderIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : C ≌ D) (X : C) : CategoryTheory.Subobject X ≃o CategoryTheory.Subobject (E.functor.obj X)

An equivalence induces an order isomorphism on the subobjects of every object.