feat(CategoryTheory/Subobject): extend image subobject API

Mathlib/CategoryTheory/Subobject/Basic.lean

@@ -12,6 +12,7 @@ public import Mathlib.CategoryTheory.ConcreteCategory.Basic
 public import Mathlib.Tactic.ApplyFun
 public import Mathlib.Tactic.CategoryTheory.Elementwise
 public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
+public import Mathlib.CategoryTheory.Category.GaloisConnection
 
 /-!
 # Subobjects
@@ -632,6 +633,10 @@ theorem isPullback (f : X ⟶ Y) (y : Subobject Y) :
     IsPullback (pullbackπ f y) ((pullback f).obj y).arrow y.arrow f :=
   (isPullback_aux f y).choose_spec
 
+lemma le_pullback_of_comm (f : X ⟶ Y) {X' : Subobject X} {Y' : Subobject Y}
+    (u : (X' : C) ⟶ Y') (h : u ≫ Y'.arrow = X'.arrow ≫ f) : X' ≤ (pullback f).obj Y' :=
+  le_of_comm ((isPullback f Y').lift u X'.arrow h) ((isPullback f Y').lift_snd u X'.arrow h)
+
 end Pullback
 
 section Map
@@ -739,12 +744,39 @@ def «exists» (f : X ⟶ Y) : Subobject X ⥤ Subobject Y :=
 theorem exists_iso_map (f : X ⟶ Y) [Mono f] : «exists» f = map f :=
   lower_iso _ _ (MonoOver.existsIsoMap f)
 
+lemma exists_eq_mk_of_mono (f : X ⟶ Y) [Mono f] (X' : Subobject X) :
+    («exists» f).obj X' = mk (X'.arrow ≫ f) := by
+  slice_lhs 0 1 => rw [exists_iso_map, ← mk_arrow X']
+  rw [map_mk]
+
+theorem exists_le_exists_iff_of_mono (f : X ⟶ Y) [Mono f] (X₁ X₂ : Subobject X) :
+    («exists» f).obj X₁ ≤ («exists» f).obj X₂ ↔ X₁ ≤ X₂ :=
+  Quotient.inductionOn₂' X₁ X₂ (fun _ _ ↦
+    ⟨fun ⟨h⟩ ↦ ⟨(MonoOver.exists f).preimage h⟩, fun ⟨h⟩ ↦ ⟨(MonoOver.exists f).map h⟩⟩)
+
 /-- `exists f : Subobject X ⥤ Subobject Y` is
 left adjoint to `pullback f : Subobject Y ⥤ Subobject X`.
 -/
 def existsPullbackAdj (f : X ⟶ Y) [HasPullbacks C] : «exists» f ⊣ pullback f :=
   lowerAdjunction (MonoOver.existsPullbackAdj f)
 
+theorem le_pullback_exists (f : X ⟶ Y) [HasPullbacks C] (X' : Subobject X) :
+    X' ≤ (pullback f).obj ((«exists» f).obj X') :=
+  (existsPullbackAdj f).gc.le_u_l X'
+
+theorem exists_pullback_le (f : X ⟶ Y) [HasPullbacks C] (Y' : Subobject Y) :
+    («exists» f).obj ((pullback f).obj Y') ≤ Y' :=
+  (existsPullbackAdj f).gc.l_u_le Y'
+
+@[simp]
+theorem pullback_exists_eq_self_of_mono (f : X ⟶ Y) [Mono f] [HasPullbacks C]
+    (X' : Subobject X) : (pullback f).obj ((«exists» f).obj X') = X' := by
+  rw [exists_iso_map, pullback_map_self]
+
+theorem exists_comp (f : X ⟶ Y) (g : Y ⟶ Z) (x : Subobject X) [HasPullbacks C] :
+    («exists» (f ≫ g)).obj x = («exists» g).obj ((«exists» f).obj x) :=
+  Quotient.inductionOn' x (fun _ ↦ Quotient.sound ⟨(MonoOver.existsComp f g).app _⟩)
+
 /--
 Taking representatives and then `MonoOver.exists` is isomorphic to taking `Subobject.exists`
 and then taking representatives.
@@ -772,6 +804,11 @@ def imageFactorisation (f : X ⟶ Y) (x : Subobject X) :
   ImageFactorisation.copy this ((«exists» f).obj x).arrow this.F.e (by
     simpa [this, -Over.w] using! (Over.w ((existsCompRepresentativeIso f).app x).hom.hom).symm)
 
+lemma exists_le_of_comm (f : X ⟶ Y) {X' : Subobject X} {Y' : Subobject Y}
+    (u : (X' : C) ⟶ Y') (h : u ≫ Y'.arrow = X'.arrow ≫ f) : («exists» f).obj X' ≤ Y' :=
+  le_of_comm ((imageFactorisation f X').isImage.lift ⟨Y', Y'.arrow, u, h⟩)
+    ((imageFactorisation f X').isImage.lift_fac _)
+
 end Exists
 
 end Subobject

Mathlib/CategoryTheory/Subobject/Lattice.lean

@@ -447,6 +447,13 @@ theorem inf_eq_map_pullback' {A : C} (f₁ : MonoOver A) (f₂ : Subobject A) :
   induction f₂ using Quotient.inductionOn'
   rfl
 
+theorem exists_pullback_eq_inf_of_mono [HasImages C] (f : X ⟶ Y) [Mono f] (Y' : Subobject Y) :
+    («exists» f).obj ((pullback f).obj Y') = Y' ⊓ mk f := by
+  rw [exists_iso_map]
+  change (map (MonoOver.mk f).arrow).obj ((pullback (MonoOver.mk f).arrow).obj Y') = _
+  rw [← inf_eq_map_pullback', inf_comm]
+  rfl
+
 theorem inf_eq_map_pullback {A : C} (f₁ : Subobject A) (f₂ : Subobject A) :
     (f₁ ⊓ f₂ : Subobject A) = (map f₁.arrow).obj ((pullback f₁.arrow).obj f₂) := by
   convert! inf_eq_map_pullback' (representative.obj f₁) f₂
@@ -510,6 +517,35 @@ theorem sup_factors_of_factors_right {A B : C} {X Y : Subobject B} {f : A ⟶ B}
     (X ⊔ Y).Factors f :=
   factors_of_le f le_sup_right P
 
+/-- If `C` has binary coproducts and `f g : Subobject A`, then `f ⨿ g ⟶ A` factors as
+  `f ⨿ g ⟶ f ⊔ g ⟶ A` -/
+@[simps]
+def supMonoFactorisation {A : C} (f g : Subobject A) : MonoFactorisation
+    (coprod.desc f.arrow g.arrow) where
+  I := underlying.obj (f ⊔ g)
+  m := (f ⊔ g).arrow
+  m_mono := inferInstance
+  e := coprod.desc (f.ofLE (f ⊔ g) le_sup_left) (g.ofLE (f ⊔ g) le_sup_right)
+  fac := by simp only [coprod.desc_comp, ofLE_arrow]
+
+/-- If `C` has binary coproducts, then `f ⊔ g` is an image of `f ⨿ g ⟶ A`. -/
+@[simps]
+def supIsImage {A : C} (f g : Subobject A) :
+    IsImage (supMonoFactorisation f g) where
+  lift F := by
+    refine (f ⊔ g).ofLEMk F.m (sup_le ?_ ?_)
+    · refine le_mk_of_comm (coprod.inl ≫ F.e) ?_
+      · simp only [assoc, MonoFactorisation.fac, coprod.inl_desc]
+    · refine le_mk_of_comm (coprod.inr ≫ F.e) ?_
+      · simp only [assoc, MonoFactorisation.fac, coprod.inr_desc]
+  lift_fac := by simp [supMonoFactorisation]
+
+/-- If `C` has binary coproducts, then `f ⊔ g ≅ image (f ⨿ g ⟶ A)`. -/
+@[simps!]
+def supIsoImage {A : C} (f g : Subobject A) : underlying.obj (f ⊔ g) ≅
+    image (coprod.desc f.arrow g.arrow) :=
+  IsImage.isoExt (supIsImage ..) <| Image.isImage _
+
 variable [HasInitial C] [InitialMonoClass C]
 
 theorem finset_sup_factors {I : Type*} {A B : C} {s : Finset I} {P : I → Subobject B} {f : A ⟶ B}

Mathlib/CategoryTheory/Subobject/Limits.lean

@@ -120,6 +120,11 @@ variable [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f]
 abbrev kernelSubobject : Subobject X :=
   Subobject.mk (kernel.ι f)
 
+lemma _root_.CategoryTheory.Subobject.pullback_kernelSubobject {W : C} (h : W ⟶ X)
+    [HasPullbacks C] [HasKernel (h ≫ f)] :
+    (Subobject.pullback h).obj (kernelSubobject f) = kernelSubobject (h ≫ f) := by
+  simpa only [kernelSubobject, comp_zero] using pullback_equalizer f 0 h
+
 /-- The underlying object of `kernelSubobject f` is (up to isomorphism!)
 the same as the chosen object `kernel f`. -/
 def kernelSubobjectIso : (kernelSubobject f : C) ≅ kernel f :=
@@ -326,6 +331,16 @@ theorem imageSubobject_arrow :
 theorem imageSubobject_arrow' :
     (imageSubobjectIso f).inv ≫ (imageSubobject f).arrow = image.ι f := by simp [imageSubobjectIso]
 
+lemma _root_.CategoryTheory.Subobject.exists_eq_imageSubobject [HasImages C]
+    (f : X ⟶ Y) (X' : Subobject X) : («exists» f).obj X' = imageSubobject (X'.arrow ≫ f) := by
+  apply eq_of_comm ((existsIsoImage f X').trans (imageSubobjectIso (X'.arrow ≫ f)).symm)
+  simp only [Iso.trans_hom, Iso.symm_hom, assoc, imageSubobject_arrow']
+  exact Over.w ((Subobject.existsCompRepresentativeIso f).app X').hom.hom
+
+lemma _root_.CategoryTheory.Subobject.exists_mk_eq_imageSubobject [HasImages C]
+    {A : C} (g : A ⟶ X) [Mono g] (f : X ⟶ Y) :
+    («exists» f).obj (mk g) = imageSubobject (g ≫ f) := by rfl
+
 /-- A factorisation of `f : X ⟶ Y` through `imageSubobject f`. -/
 def factorThruImageSubobject : X ⟶ imageSubobject f :=
   factorThruImage f ≫ (imageSubobjectIso f).inv
@@ -363,6 +378,25 @@ theorem imageSubobject_comp_le {X' : C} (h : X' ⟶ X) (f : X ⟶ Y) [HasImage f
     imageSubobject (h ≫ f) ≤ imageSubobject f :=
   Subobject.mk_le_mk_of_comm (image.preComp h f) (by simp)
 
+theorem imageSubobject_epi_comp [HasStrongEpiMonoFactorisations C] {X Y X' : C}
+    (e : X' ⟶ X) (f : X ⟶ Y) [StrongEpi e] [Mono f] :
+    imageSubobject (e ≫ f) = imageSubobject f :=
+  mk_eq_mk_of_comm (image.ι (e ≫ f)) (image.ι f)
+    ((image.isoStrongEpiMono e f rfl).symm ≪≫
+      (image.isoStrongEpiMono (𝟙 _) f (Category.id_comp _))) (by simp)
+
+lemma _root_.CategoryTheory.Subobject.sup_eq_imageSubobject [HasImages C] [HasBinaryCoproducts C]
+    {A : C} (X Y : Subobject A) :
+    X ⊔ Y = imageSubobject (coprod.desc X.arrow Y.arrow) :=
+  eq_mk_of_comm (image.ι (coprod.desc X.arrow Y.arrow)) (supIsoImage X Y) (ofLEMk_comp _)
+
+lemma _root_.CategoryTheory.Subobject.mk_mono_eq_imageSubobject [HasStrongEpiMonoFactorisations C]
+    {X Y : C} {f : X ⟶ Y} {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f)
+    [StrongEpi e] [Mono m] :
+    mk m = imageSubobject f :=
+  mk_eq_mk_of_comm m (image.ι f) (image.isoStrongEpiMono e m comm)
+    (image.isoStrongEpiMono_hom_comp_ι e m comm)
+
 section
 
 variable [HasZeroMorphisms C] [HasZeroObject C]

Mathlib/CategoryTheory/Subobject/MonoOver.lean

@@ -501,13 +501,56 @@ def existsIsoMap (f : X ⟶ Y) [Mono f] : «exists» f ≅ map f :=
     · apply imageMonoIsoSource (Z.arrow ≫ f)
     · apply imageMonoIsoSource_hom_self)
 
-/-- `exists` is adjoint to `pullback` when images exist -/
+instance full_exists (f : X ⟶ Y) [Mono f] : Functor.Full («exists» f) :=
+  Functor.Full.of_iso (existsIsoMap f).symm
+
+/-- `exists` is left adjoint to `pullback` when images exist -/
 def existsPullbackAdj (f : X ⟶ Y) [HasPullbacks C] : «exists» f ⊣ pullback f :=
   ((Over.mapPullbackAdj f).comp imageForgetAdj).restrictFullyFaithful
     (fullyFaithfulForget X) (Functor.FullyFaithful.id _) (Iso.refl _) (Iso.refl _)
 
+set_option backward.isDefEq.respectTransparency false in
+@[reassoc (attr := simp)]
+lemma factorThruImage_comp_existsPullbackAdj_counit_app_hom_left
+    (f : X ⟶ Y) [HasPullbacks C] (B : MonoOver Y) :
+    factorThruImage (pullback.snd B.arrow f ≫ f) ≫
+        ((existsPullbackAdj f).counit.app B).hom.left = pullback.fst B.arrow f := by
+  have hw : ((existsPullbackAdj f).counit.app B).hom.left ≫ B.arrow =
+      image.ι (pullback.snd B.arrow f ≫ f) :=
+    MonoOver.w ((existsPullbackAdj f).counit.app B)
+  rw [← cancel_mono B.arrow, Category.assoc, hw, image.fac, pullback.condition]
+
+/-- `MonoOver.exists` commutes with composition (up to isomorphism). -/
+def existsComp (f : X ⟶ Y) (g : Y ⟶ Z) [HasPullbacks C] :
+    «exists» (f ≫ g) ≅ «exists» f ⋙ «exists» g :=
+  ((conjugateIsoEquiv (existsPullbackAdj (f ≫ g))
+    ((existsPullbackAdj f).comp (existsPullbackAdj g))).symm (pullbackComp f g)).symm
+
 end Exists
 
+section HasStrongEpiMonoFactorisations
+
+variable [HasStrongEpiMonoFactorisations C]
+
+/-- Given a strong epi-mono factorization of `f : Over X` as `e ≫ m`, the image of `f` is
+isomorphic to `MonoOver.mk m`. -/
+@[simps!]
+def imageObjIso (f : Over X)
+    {Z : C} (e : f.left ⟶ Z) [StrongEpi e] (m : Z ⟶ X) [Mono m] (fac : e ≫ m = f.hom) :
+    image.obj f ≅ MonoOver.mk m :=
+  MonoOver.isoMk (image.isoStrongEpiMono e m fac).symm
+    (image.isoStrongEpiMono_inv_comp_mono e m fac)
+
+/-- Given `p : X ⟶ Y`, `f : MonoOver X`, and a strong-epi-mono factorization of
+`f.arrow ≫ p` as `e ≫ m`, `(exists p).obj f` is isomorphic to `MonoOver.mk m`. -/
+@[simps!]
+def existsObjIso (p : X ⟶ Y) (f : MonoOver X)
+    {Z : C} (e : f.obj.left ⟶ Z) [StrongEpi e] (m : Z ⟶ Y) [Mono m] (fac : e ≫ m = f.arrow ≫ p) :
+    («exists» p).obj f ≅ MonoOver.mk m :=
+  imageObjIso (Over.mk (f.arrow ≫ p)) e m fac
+
+end HasStrongEpiMonoFactorisations
+
 end MonoOver
 
 end CategoryTheory