feat(CategoryTheory): pushforward pullback adjunction for P.Over Q X (#19271)

Author: chrisflav

Mathlib.lean

@@ -1991,6 +1991,7 @@ import Mathlib.CategoryTheory.MorphismProperty.Concrete
 import Mathlib.CategoryTheory.MorphismProperty.Factorization
 import Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
 import Mathlib.CategoryTheory.MorphismProperty.Limits
+import Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
 import Mathlib.CategoryTheory.MorphismProperty.Representable
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.NatTrans

Mathlib/CategoryTheory/Limits/MorphismProperty.lean

@@ -119,9 +119,8 @@ instance [P.ContainsIdentities] (Y : P.Over ⊤ X) :
   uniq a := by
     ext
     · simp only [mk_left, Hom.hom_left, homMk_hom, Over.homMk_left]
-      rw [← Over.w a.hom]
+      rw [← Over.w a]
       simp only [mk_left, Functor.const_obj_obj, Hom.hom_left, mk_hom, Category.comp_id]
-    · rfl
 
 /-- `X ⟶ X` is the terminal object of `P.Over ⊤ X`. -/
 def mkIdTerminal [P.ContainsIdentities] :

Mathlib/CategoryTheory/MorphismProperty/Basic.lean

@@ -157,6 +157,10 @@ lemma RespectsIso.precomp (P : MorphismProperty C) [P.RespectsIso] {X Y Z : C} (
     [IsIso e] (f : Y ⟶ Z) (hf : P f) : P (e ≫ f) :=
   RespectsLeft.precomp (Q := isomorphisms C) e ‹IsIso e› f hf
 
+instance : RespectsIso (⊤ : MorphismProperty C) where
+  precomp _ _ _ _ := trivial
+  postcomp _ _ _ _ := trivial
+
 lemma RespectsIso.postcomp (P : MorphismProperty C) [P.RespectsIso] {X Y Z : C} (e : Y ⟶ Z)
     [IsIso e] (f : X ⟶ Y) (hf : P f) : P (f ≫ e) :=
   RespectsRight.postcomp (Q := isomorphisms C) e ‹IsIso e› f hf

Mathlib/CategoryTheory/MorphismProperty/Comma.lean

@@ -79,10 +79,8 @@ lemma Hom.hom_mk {X Y : P.Comma L R Q W}
     (f : CommaMorphism X.toComma Y.toComma) (hf) (hg) :
   Comma.Hom.hom ⟨f, hf, hg⟩ = f := rfl
 
-@[simp]
 lemma Hom.hom_left {X Y : P.Comma L R Q W} (f : Comma.Hom X Y) : f.hom.left = f.left := rfl
 
-@[simp]
 lemma Hom.hom_right {X Y : P.Comma L R Q W} (f : Comma.Hom X Y) : f.hom.right = f.right := rfl
 
 /-- See Note [custom simps projection] -/
@@ -133,6 +131,14 @@ lemma id_hom (X : P.Comma L R Q W) : (𝟙 X : X ⟶ X).hom = 𝟙 X.toComma :=
 lemma comp_hom {X Y Z : P.Comma L R Q W} (f : X ⟶ Y) (g : Y ⟶ Z) :
     (f ≫ g).hom = f.hom ≫ g.hom := rfl
 
+@[reassoc]
+lemma comp_left {X Y Z : P.Comma L R Q W} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    (f ≫ g).left = f.left ≫ g.left := rfl
+
+@[reassoc]
+lemma comp_right {X Y Z : P.Comma L R Q W} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    (f ≫ g).right = f.right ≫ g.right := rfl
+
 /-- If `i` is an isomorphism in `Comma L R`, it is also a morphism in `P.Comma L R Q W`. -/
 @[simps hom]
 def homFromCommaOfIsIso [Q.RespectsIso] [W.RespectsIso] {X Y : P.Comma L R Q W}
@@ -205,6 +211,63 @@ def forgetFullyFaithful : (forget L R P ⊤ ⊤).FullyFaithful where
 instance : (forget L R P ⊤ ⊤).Full :=
   Functor.FullyFaithful.full (forgetFullyFaithful L R P)
 
+section
+
+variable {L R}
+
+@[simp]
+lemma eqToHom_left {X Y : P.Comma L R Q W} (h : X = Y) :
+    (eqToHom h).left = eqToHom (by rw [h]) := by
+  subst h
+  rfl
+
+@[simp]
+lemma eqToHom_right {X Y : P.Comma L R Q W} (h : X = Y) :
+    (eqToHom h).right = eqToHom (by rw [h]) := by
+  subst h
+  rfl
+
+end
+
+section Functoriality
+
+variable {L R P Q W}
+variable {L₁ L₂ L₃ : A ⥤ T} {R₁ R₂ R₃ : B ⥤ T}
+
+/-- Lift a functor `F : C ⥤ Comma L R` to the subcategory `P.Comma L R Q W` under
+suitable assumptions on `F`. -/
+@[simps obj_toComma map_hom]
+def lift {C : Type*} [Category C] (F : C ⥤ Comma L R)
+    (hP : ∀ X, P (F.obj X).hom)
+    (hQ : ∀ {X Y} (f : X ⟶ Y), Q (F.map f).left)
+    (hW : ∀ {X Y} (f : X ⟶ Y), W (F.map f).right) :
+    C ⥤ P.Comma L R Q W where
+  obj X :=
+    { __ := F.obj X
+      prop := hP X }
+  map {X Y} f :=
+    { __ := F.map f
+      prop_hom_left := hQ f
+      prop_hom_right := hW f }
+
+variable (R) in
+/-- A natural transformation `L₁ ⟶ L₂` induces a functor `P.Comma L₂ R Q W ⥤ P.Comma L₁ R Q W`. -/
+@[simps!]
+def mapLeft (l : L₁ ⟶ L₂) (hl : ∀ X : P.Comma L₂ R Q W, P (l.app X.left ≫ X.hom)) :
+    P.Comma L₂ R Q W ⥤ P.Comma L₁ R Q W :=
+  lift (forget _ _ _ _ _ ⋙ CategoryTheory.Comma.mapLeft R l) hl
+    (fun f ↦ f.prop_hom_left) (fun f ↦ f.prop_hom_right)
+
+variable (L) in
+/-- A natural transformation `R₁ ⟶ R₂` induces a functor `P.Comma L R₁ Q W ⥤ P.Comma L R₂ Q W`. -/
+@[simps!]
+def mapRight (r : R₁ ⟶ R₂) (hr : ∀ X : P.Comma L R₁ Q W, P (X.hom ≫ r.app X.right)) :
+    P.Comma L R₁ Q W ⥤ P.Comma L R₂ Q W :=
+  lift (forget _ _ _ _ _ ⋙ CategoryTheory.Comma.mapRight L r) hr
+    (fun f ↦ f.prop_hom_left) (fun f ↦ f.prop_hom_right)
+
+end Functoriality
+
 end Comma
 
 end Comma
@@ -251,6 +314,23 @@ protected def Over.homMk {A B : P.Over Q X} (f : A.left ⟶ B.left)
   prop_hom_left := hf
   prop_hom_right := trivial
 
+/-- Make an isomorphism in `P.Over Q X` from an isomorphism in `T` with compatibilities. -/
+@[simps! hom_left inv_left]
+protected def Over.isoMk [Q.RespectsIso] {A B : P.Over Q X} (f : A.left ≅ B.left)
+    (w : f.hom ≫ B.hom = A.hom := by aesop_cat) : A ≅ B :=
+  Comma.isoMk f (Discrete.eqToIso' rfl)
+
+@[ext]
+lemma Over.Hom.ext {A B : P.Over Q X} {f g : A ⟶ B} (h : f.left = g.left) : f = g := by
+  ext
+  · exact h
+  · simp
+
+@[reassoc]
+lemma Over.w {A B : P.Over Q X} (f : A ⟶ B) :
+    f.left ≫ B.hom = A.hom := by
+  simp
+
 end Over
 
 section Under
@@ -295,6 +375,23 @@ protected def Under.homMk {A B : P.Under Q X} (f : A.right ⟶ B.right)
   prop_hom_left := trivial
   prop_hom_right := hf
 
+/-- Make an isomorphism in `P.Under Q X` from an isomorphism in `T` with compatibilities. -/
+@[simps! hom_right inv_right]
+protected def Under.isoMk [Q.RespectsIso] {A B : P.Under Q X} (f : A.right ≅ B.right)
+    (w : A.hom ≫ f.hom = B.hom := by aesop_cat) : A ≅ B :=
+  Comma.isoMk (Discrete.eqToIso' rfl) f
+
+@[ext]
+lemma Under.Hom.ext {A B : P.Under Q X} {f g : A ⟶ B} (h : f.right = g.right) : f = g := by
+  ext
+  · simp
+  · exact h
+
+@[reassoc]
+lemma Under.w {A B : P.Under Q X} (f : A ⟶ B) :
+    A.hom ≫ f.right = B.hom := by
+  simp
+
 end Under
 
 end CategoryTheory.MorphismProperty

Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean

@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2024 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+import Mathlib.CategoryTheory.MorphismProperty.Comma
+import Mathlib.CategoryTheory.Adjunction.Over
+import Mathlib.CategoryTheory.MorphismProperty.Limits
+
+/-!
+# Adjunction of pushforward and pullback in `P.Over Q X`
+
+A morphism `f : X ⟶ Y` defines two functors:
+
+- `Over.map`: post-composition with `f`
+- `Over.pullback`: base-change along `f`
+
+These are adjoint under suitable assumptions on `P` and `Q`.
+
+-/
+
+namespace CategoryTheory.MorphismProperty
+
+open Limits
+
+variable {T : Type*} [Category T] (P Q : MorphismProperty T) [Q.IsMultiplicative]
+variable {X Y : T} (f : X ⟶ Y)
+
+section Map
+
+variable {P} [P.IsStableUnderComposition] (hPf : P f)
+
+variable {f}
+
+/-- If `P` is stable under composition and `f : X ⟶ Y` satisfies `P`,
+this is the functor `P.Over Q X ⥤ P.Over Q Y` given by composing with `f`. -/
+@[simps! obj_left obj_hom map_left]
+def Over.map : P.Over Q X ⥤ P.Over Q Y :=
+  Comma.mapRight _ (Discrete.natTrans fun _ ↦ f) <| fun X ↦ P.comp_mem _ _ X.prop hPf
+
+lemma Over.map_comp {X Y Z : T} {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) :
+    map Q (P.comp_mem f g hf hg) = map Q hf ⋙ map Q hg := by
+  fapply Functor.ext
+  · simp [map, Comma.mapRight, CategoryTheory.Comma.mapRight, Comma.lift]
+  · intro U V k
+    ext
+    simp
+
+/-- `Over.map` commutes with composition. -/
+@[simps! hom_app_left inv_app_left]
+def Over.mapComp {X Y Z : T} {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [Q.RespectsIso] :
+    map Q (P.comp_mem f g hf hg) ≅ map Q hf ⋙ map Q hg :=
+  NatIso.ofComponents (fun X ↦ Over.isoMk (Iso.refl _))
+
+end Map
+
+section Pullback
+
+variable [HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange]
+
+/-- If `P` and `Q` are stable under base change and pullbacks exist in `T`,
+this is the functor `P.Over Q Y ⥤ P.Over Q X` given by base change along `f`. -/
+@[simps! obj_left obj_hom map_left]
+noncomputable def Over.pullback : P.Over Q Y ⥤ P.Over Q X where
+  obj A :=
+    { __ := (CategoryTheory.Over.pullback f).obj A.toComma
+      prop := P.pullback_snd _ _ A.prop }
+  map {A B} g :=
+    { __ := (CategoryTheory.Over.pullback f).map g.toCommaMorphism
+      prop_hom_left := Q.baseChange_map f g.toCommaMorphism g.prop_hom_left
+      prop_hom_right := trivial }
+
+variable {P} {Q}
+
+/-- `Over.pullback` commutes with composition. -/
+@[simps! hom_app_left inv_app_left]
+noncomputable def Over.pullbackComp [Q.RespectsIso] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    Over.pullback P Q (f ≫ g) ≅ Over.pullback P Q g ⋙ Over.pullback P Q f :=
+  NatIso.ofComponents
+    (fun X ↦ Over.isoMk ((pullbackLeftPullbackSndIso X.hom g f).symm) (by simp))
+
+lemma Over.pullbackComp_left_fst_fst [Q.RespectsIso] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z)
+    (A : P.Over Q Z) :
+    ((Over.pullbackComp f g).hom.app A).left ≫
+      pullback.fst (pullback.snd A.hom g) f ≫ pullback.fst A.hom g =
+        pullback.fst A.hom (f ≫ g) := by
+  simp
+
+/-- If `f = g`, then base change along `f` is naturally isomorphic to base change along `g`. -/
+noncomputable def Over.pullbackCongr {X Y : T} {f g : X ⟶ Y} (h : f = g) :
+    Over.pullback P Q f ≅ Over.pullback P Q g :=
+  NatIso.ofComponents (fun X ↦ eqToIso (by rw [h]))
+
+@[reassoc (attr := simp)]
+lemma Over.pullbackCongr_hom_app_left_fst {X Y : T} {f g : X ⟶ Y} (h : f = g) (A : P.Over Q Y) :
+    ((Over.pullbackCongr h).hom.app A).left ≫ pullback.fst A.hom g =
+      pullback.fst A.hom f := by
+  subst h
+  simp [pullbackCongr]
+
+end Pullback
+
+section Adjunction
+
+variable [P.IsStableUnderComposition] [P.IsStableUnderBaseChange]
+  [Q.IsStableUnderBaseChange] [HasPullbacks T]
+
+/-- `P.Over.map` is left adjoint to `P.Over.pullback` if `f` satisfies `P`. -/
+noncomputable def Over.mapPullbackAdj [Q.HasOfPostcompProperty Q] (hPf : P f) (hQf : Q f) :
+    Over.map Q hPf ⊣ Over.pullback P Q f :=
+  Adjunction.mkOfHomEquiv
+    { homEquiv := fun A B ↦
+        { toFun := fun g ↦
+            Over.homMk (pullback.lift g.left A.hom <| by simp) (by simp) <| by
+              apply Q.of_postcomp (W' := Q)
+              · exact Q.pullback_fst B.hom f hQf
+              · simpa using g.prop_hom_left
+          invFun := fun h ↦ Over.homMk (h.left ≫ pullback.fst B.hom f)
+            (by
+              simp only [map_obj_left, Functor.const_obj_obj, pullback_obj_left, Functor.id_obj,
+                Category.assoc, pullback.condition, map_obj_hom, ← pullback_obj_hom, Over.w_assoc])
+            (Q.comp_mem _ _ h.prop_hom_left (Q.pullback_fst _ _ hQf))
+          left_inv := by aesop_cat
+          right_inv := fun h ↦ by
+            ext
+            dsimp
+            ext
+            · simp
+            · simpa using h.w.symm } }
+
+end Adjunction
+
+end CategoryTheory.MorphismProperty