Object properties: transport along equivalences, and closure properties

This file contains general lemmas about object properties: transporting them along an equivalence, comparing Mathlib's closure type classes with one another in the presence of a zero object and of binary biproducts, smallness of full subcategories, and additivity of the standard functors between full subcategories.

Main declarations

• CategoryTheory.ObjectProperty.inverseImage_functor_inverseImage_inverse: pulling an isomorphism-invariant property backward along both functors of an equivalence recovers it.
• CategoryTheory.ObjectProperty.isClosedUnderIsomorphisms_of_containsZero: a property holding for a zero object and closed under binary products is closed under isomorphisms.
• CategoryTheory.ObjectProperty.isClosedUnderBinaryProducts_of_prop_biprod: for a replete property in a category with binary biproducts, closure under binary products only has to be checked on biproducts.
• CategoryTheory.ObjectProperty.prop_biprod_of_isClosedUnderBinaryProducts: a property closed under binary products holds for binary biproducts, with X ⊞ Y as the syntactic form of the conclusion.
• CategoryTheory.ObjectProperty.essentiallySmall_of_ambient: every property in an essentially small category is essentially small.
• CategoryTheory.ObjectProperty.ιOfLE_additive: the inclusion of a smaller property into a larger one is additive.
• CategoryTheory.Equivalence.congrFullSubcategory_functor_additive and CategoryTheory.Equivalence.congrFullSubcategory_inverse_additive: an additive equivalence restricts to an additive equivalence between corresponding full subcategories.
• CategoryTheory.Equivalence.congrFullSubcategory_functor_comp_ι and CategoryTheory.Equivalence.congrFullSubcategory_inverse_comp_ι: the restricted functors, followed by the inclusions, are the inclusions followed by the original functors.
• CategoryTheory.Equivalence.congrFullSubcategory_functor_obj_obj, CategoryTheory.Equivalence.congrFullSubcategory_functor_map_hom and their inverse counterparts: the restricted functors evaluated on objects and morphisms, for deriving the evaluation lemmas of any equivalence defined as a congrFullSubcategory.

theorem CategoryTheory.ObjectProperty.inverseImage_functor_inverseImage_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] (e : C ≌ D) : (P.inverseImage e.inverse).inverseImage e.functor = P

Pulling an isomorphism-invariant object property backward along both functors of an equivalence recovers the original property.

theorem CategoryTheory.ObjectProperty.isClosedUnderIsomorphisms_of_containsZero {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderBinaryProducts] : P.IsClosedUnderIsomorphisms

A property holding for a zero object and closed under binary products is closed under isomorphisms. An isomorphism e : X ≅ Y exhibits Y as a product of a zero object with X, the two projections being the zero morphism and e.inv.

Mathlib's CategoryTheory.ObjectProperty.IsClosedUnderBinaryProducts.closedUnderIsomorphisms is the same argument run on a terminal object, but it assumes closure under the empty limit, which CategoryTheory.ObjectProperty.ContainsZero — the property for one zero object — does not supply before repleteness is known.

theorem CategoryTheory.ObjectProperty.isClosedUnderBinaryProducts_of_prop_biprod {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] (h : ∀ (X Y : C), P X → P Y → P (X ⊞ Y)) : P.IsClosedUnderBinaryProducts

For a replete property, closure under binary products only has to be checked on biproducts, since in a category with binary biproducts every binary product is one.

theorem CategoryTheory.ObjectProperty.prop_biprod_of_isClosedUnderBinaryProducts {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) [P.IsClosedUnderBinaryProducts] {X Y : C} [Limits.HasBinaryBiproduct X Y] (hX : P X) (hY : P Y) : P (X ⊞ Y)

A property closed under binary products holds for binary biproducts. In a category with binary biproducts the biproduct is a binary product, so this is CategoryTheory.ObjectProperty.prop_of_isLimit_binaryFan applied to CategoryTheory.Limits.BinaryBiproduct.isLimit; naming it keeps the index of the conclusion syntactically X ⊞ Y, which matters when the conclusion is the type index of a dependent family.

instance CategoryTheory.ObjectProperty.essentiallySmall_of_ambient {C : Type u₁} [Category.{v₁, u₁} C] [EssentiallySmall.{w, v₁, u₁} C] (P : ObjectProperty C) : ObjectProperty.EssentiallySmall.{w, v₁, u₁} P

Every object property in an essentially small category is essentially small. This supplies the smallness instance for its full subcategory through Mathlib's object-property API.

instance CategoryTheory.ObjectProperty.ιOfLE_additive {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {P P' : ObjectProperty C} (h : P ≤ P') : (ιOfLE h).Additive

The inclusion of a smaller object property into a larger one is an additive functor: both categories carry the addition of the ambient one.

theorem CategoryTheory.Equivalence.congrFullSubcategory_functor_eq_lift {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P : ObjectProperty C} {Q : ObjectProperty D} [Q.IsClosedUnderIsomorphisms] (e : C ≌ D) (h : Q.inverseImage e.functor = P) : (e.congrFullSubcategory h).functor = Q.lift (P.ι.comp e.functor) ⋯

The forward functor on corresponding full subcategories is the lift of the original functor.

theorem CategoryTheory.Equivalence.congrFullSubcategory_inverse_eq_lift {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P : ObjectProperty C} {Q : ObjectProperty D} [Q.IsClosedUnderIsomorphisms] (e : C ≌ D) (h : Q.inverseImage e.functor = P) : (e.congrFullSubcategory h).inverse = P.lift (Q.ι.comp e.inverse) ⋯

The inverse functor on corresponding full subcategories is the lift of the original inverse.

theorem CategoryTheory.Equivalence.congrFullSubcategory_functor_comp_ι {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P : ObjectProperty C} {Q : ObjectProperty D} [Q.IsClosedUnderIsomorphisms] (e : C ≌ D) (h : Q.inverseImage e.functor = P) : (e.congrFullSubcategory h).functor.comp Q.ι = P.ι.comp e.functor

The forward functor on corresponding full subcategories, followed by the inclusion, is the inclusion followed by the original functor.

theorem CategoryTheory.Equivalence.congrFullSubcategory_inverse_comp_ι {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P : ObjectProperty C} {Q : ObjectProperty D} [Q.IsClosedUnderIsomorphisms] (e : C ≌ D) (h : Q.inverseImage e.functor = P) : (e.congrFullSubcategory h).inverse.comp P.ι = Q.ι.comp e.inverse

The inverse functor on corresponding full subcategories, followed by the inclusion, is the inclusion followed by the original inverse.

theorem CategoryTheory.Equivalence.congrFullSubcategory_functor_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P : ObjectProperty C} {Q : ObjectProperty D} [Q.IsClosedUnderIsomorphisms] (e : C ≌ D) (h : Q.inverseImage e.functor = P) (X : P.FullSubcategory) : ((e.congrFullSubcategory h).functor.obj X).obj = e.functor.obj X.obj

The forward functor on corresponding full subcategories acts on objects as the original functor. Not a simp lemma: congrFullSubcategory_functor already unfolds the left-hand side.

theorem CategoryTheory.Equivalence.congrFullSubcategory_functor_map_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P : ObjectProperty C} {Q : ObjectProperty D} [Q.IsClosedUnderIsomorphisms] (e : C ≌ D) (h : Q.inverseImage e.functor = P) {X Y : P.FullSubcategory} (f : X ⟶ Y) : ((e.congrFullSubcategory h).functor.map f).hom = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (e.functor.map f.hom) (eqToHom ⋯))

The forward functor on corresponding full subcategories acts on morphisms as the original functor, up to the identifications of congrFullSubcategory_functor_obj_obj.

theorem CategoryTheory.Equivalence.congrFullSubcategory_inverse_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P : ObjectProperty C} {Q : ObjectProperty D} [Q.IsClosedUnderIsomorphisms] (e : C ≌ D) (h : Q.inverseImage e.functor = P) (Y : Q.FullSubcategory) : ((e.congrFullSubcategory h).inverse.obj Y).obj = e.inverse.obj Y.obj

The inverse functor on corresponding full subcategories acts on objects as the original inverse. Not a simp lemma: congrFullSubcategory_inverse already unfolds the left-hand side.

theorem CategoryTheory.Equivalence.congrFullSubcategory_inverse_map_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P : ObjectProperty C} {Q : ObjectProperty D} [Q.IsClosedUnderIsomorphisms] (e : C ≌ D) (h : Q.inverseImage e.functor = P) {X Y : Q.FullSubcategory} (f : X ⟶ Y) : ((e.congrFullSubcategory h).inverse.map f).hom = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (e.inverse.map f.hom) (eqToHom ⋯))

The inverse functor on corresponding full subcategories acts on morphisms as the original inverse, up to the identifications of congrFullSubcategory_inverse_obj_obj.

instance CategoryTheory.Equivalence.congrFullSubcategory_functor_additive {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] {P : ObjectProperty C} {Q : ObjectProperty D} [Q.IsClosedUnderIsomorphisms] (e : C ≌ D) [e.functor.Additive] (h : Q.inverseImage e.functor = P) : (e.congrFullSubcategory h).functor.Additive

The functor of an equivalence restricted to corresponding full subcategories is additive.

instance CategoryTheory.Equivalence.congrFullSubcategory_inverse_additive {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] {P : ObjectProperty C} {Q : ObjectProperty D} [Q.IsClosedUnderIsomorphisms] (e : C ≌ D) [e.inverse.Additive] (h : Q.inverseImage e.functor = P) : (e.congrFullSubcategory h).inverse.Additive

The inverse of an equivalence restricted to corresponding full subcategories is additive.