[Merged by Bors] - feat(CategoryTheory/ObjectProperty): various additions

Mathlib/CategoryTheory/Limits/Shapes/ZeroObjects.lean

@@ -215,6 +215,14 @@ theorem IsZero.obj [HasZeroObject D] {F : C ⥤ D} (hF : IsZero F) (X : C) : IsZ
   let e : F ≅ G := hF.iso hG
   exact (isZero_zero _).of_iso (e.app X)
 
+lemma IsZero.of_full_of_faithful_of_isZero
+    (F : C ⥤ D) [F.Full] [F.Faithful] (X : C) (hX : IsZero (F.obj X)) :
+    IsZero X := by
+  have h : F.FullyFaithful := .ofFullyFaithful _
+  have (Y : C) := (hX.unique_to (F.obj Y)).some
+  have (Y : C) := (hX.unique_from (F.obj Y)).some
+  exact ⟨fun Y ↦ ⟨h.homEquiv.unique⟩, fun Y ↦ ⟨h.homEquiv.unique⟩⟩
+
 namespace HasZeroObject
 
 variable [HasZeroObject C]

Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean

@@ -6,6 +6,8 @@ Authors: Joël Riou
 module
 
 public import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
+public import Mathlib.CategoryTheory.ObjectProperty.Opposite
+public import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
 public import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
 
 /-!
@@ -24,13 +26,13 @@ universe v v' u u'
 
 namespace CategoryTheory
 
-open Limits ZeroObject
+open Limits ZeroObject Opposite
 
 variable {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D]
 
 namespace ObjectProperty
 
-variable (P : ObjectProperty C)
+variable (P Q : ObjectProperty C)
 
 /-- Given `P : ObjectProperty C`, we say that `P.ContainsZero` if there exists
 a zero object for which `P` holds. When `P` is closed under isomorphisms,
@@ -76,6 +78,27 @@ instance [P.ContainsZero] : P.isoClosure.ContainsZero where
     obtain ⟨Z, hZ, hP⟩ := P.exists_prop_of_containsZero
     exact ⟨Z, hZ, P.le_isoClosure _ hP⟩
 
+instance [P.ContainsZero] [P.IsClosedUnderIsomorphisms] [Q.ContainsZero] :
+    (P ⊓ Q).ContainsZero where
+  exists_zero := by
+    obtain ⟨Z, hZ, hQ⟩ := Q.exists_prop_of_containsZero
+    exact ⟨Z, hZ, P.prop_of_isZero hZ, hQ⟩
+
+instance [P.ContainsZero] : P.op.ContainsZero where
+  exists_zero := by
+    obtain ⟨Z, hZ, mem⟩ := P.exists_prop_of_containsZero
+    exact ⟨op Z, hZ.op, mem⟩
+
+instance (P : ObjectProperty Cᵒᵖ) [P.ContainsZero] : P.unop.ContainsZero where
+  exists_zero := by
+    obtain ⟨Z, hZ, mem⟩ := P.exists_prop_of_containsZero
+    exact ⟨Z.unop, hZ.unop, mem⟩
+
+instance [P.ContainsZero] : HasZeroObject P.FullSubcategory where
+  zero := by
+    obtain ⟨X, h₁, h₂⟩ := P.exists_prop_of_containsZero
+    exact ⟨_, IsZero.of_full_of_faithful_of_isZero P.ι ⟨X, h₂⟩ h₁⟩
+
 end ObjectProperty
 
 /-- Given a functor `F : C ⥤ D`, this is the property of objects of `C`

Mathlib/CategoryTheory/ObjectProperty/FullSubcategory.lean

@@ -63,6 +63,8 @@ theorem ι_obj {X} : P.ι.obj X = X.obj :=
 theorem ι_map {X Y} {f : X ⟶ Y} : P.ι.map f = f.hom :=
   rfl
 
+lemma prop_ι_obj (X) : P (P.ι.obj X) := X.2
+
 @[simp]
 lemma FullSubcategory.id_hom (X : P.FullSubcategory) :
     InducedCategory.Hom.hom (𝟙 X) = 𝟙 X.obj := rfl
@@ -80,6 +82,11 @@ variable {P} in
 def homMk {X Y : P.FullSubcategory} (f : X.obj ⟶ Y.obj) : X ⟶ Y where
   hom := f
 
+variable {P} in
+lemma homMk_surjective {X Y : P.FullSubcategory} :
+    Function.Surjective (homMk : (X.obj ⟶ Y.obj) → _) :=
+  fun f ↦ ⟨f.hom, rfl⟩
+
 /-- The inclusion of a full subcategory is fully faithful. -/
 abbrev fullyFaithfulι :
     P.ι.FullyFaithful where

Mathlib/CategoryTheory/ObjectProperty/Shift.lean

@@ -24,7 +24,7 @@ open CategoryTheory Category
 
 namespace CategoryTheory
 
-variable {C : Type*} [Category* C] (P : ObjectProperty C)
+variable {C : Type*} [Category* C] (P Q : ObjectProperty C)
   {A : Type*} [AddMonoid A] [HasShift C A]
 
 namespace ObjectProperty
@@ -67,6 +67,11 @@ instance (a : A) [P.IsStableUnderShiftBy a] :
     rintro X ⟨Y, hY, ⟨e⟩⟩
     exact ⟨Y⟦a⟧, P.le_shift a _ hY, ⟨(shiftFunctor C a).mapIso e⟩⟩
 
+instance (a : A) [P.IsStableUnderShiftBy a]
+    [Q.IsStableUnderShiftBy a] : (P ⊓ Q).IsStableUnderShiftBy a where
+  le_shift _ hX :=
+    ⟨P.le_shift a _ hX.1, Q.le_shift a _ hX.2⟩
+
 variable (A) in
 /-- `P : ObjectProperty C` is stable under the shift by `A` if
 `P X` implies `P X⟦a⟧` for any `a : A`. -/
@@ -78,6 +83,9 @@ attribute [instance] IsStableUnderShift.isStableUnderShiftBy
 instance [P.IsStableUnderShift A] :
     P.isoClosure.IsStableUnderShift A where
 
+instance [P.IsStableUnderShift A]
+    [Q.IsStableUnderShift A] : (P ⊓ Q).IsStableUnderShift A where
+
 lemma prop_shift_iff_of_isStableUnderShift {G : Type*} [AddGroup G] [HasShift C G]
     [P.IsStableUnderShift G] [P.IsClosedUnderIsomorphisms] (X : C) (g : G) :
     P (X⟦g⟧) ↔ P X := by