refactor(category_theory/morphism_property): stable_under_base_change (…

…#16196)

This PR redefines `morphism_property.stable_under_base_change P`. This condition now states that for all pullback squares (`is_pullback`), the left map satisfies the property if the right map does. Then, it is automatic that the property `P` respects isos. A constructor is provided to take as an input the assumption that `P` respects isos and the previous condition that if a map `g` satisfies `P`, then `pullback.fst : pullback f g → _` satisfies it `P`.

src/algebraic_geometry/morphisms/basic.lean

@@ -413,9 +413,10 @@ end
 
 lemma is_local.stable_under_base_change
   {P : affine_target_morphism_property} (hP : P.is_local) (hP' : P.stable_under_base_change) :
-  (target_affine_locally P).stable_under_base_change  :=
+  (target_affine_locally P).stable_under_base_change :=
+morphism_property.stable_under_base_change.mk (target_affine_locally_respects_iso hP.respects_iso)
 begin
-  introv X H,
+  intros X Y S f g H,
   rw (hP.target_affine_locally_is_local.open_cover_tfae (pullback.fst : pullback f g ⟶ X)).out 0 1,
   use S.affine_cover.pullback_cover f,
   intro i,

src/category_theory/limits/shapes/comm_sq.lean

@@ -213,6 +213,13 @@ lemma of_iso_pullback (h : comm_sq fst snd f g) [has_pullback f g] (i : P ≅ pu
 of_is_limit' h (limits.is_limit.of_iso_limit (limit.is_limit _)
   (@pullback_cone.ext _ _ _ _ _ _ _ (pullback_cone.mk _ _ _) _ i w₁.symm w₂.symm).symm)
 
+lemma of_horiz_is_iso [is_iso fst] [is_iso g] (sq : comm_sq fst snd f g) :
+  is_pullback fst snd f g := of_is_limit' sq
+begin
+  refine pullback_cone.is_limit.mk _ (λ s, s.fst ≫ inv fst) (by tidy) (λ s, _) (by tidy),
+  simp only [← cancel_mono g, category.assoc, ← sq.w, is_iso.inv_hom_id_assoc, s.condition],
+end
+
 end is_pullback
 
 namespace is_pushout
@@ -375,6 +382,9 @@ is_pushout.of_is_colimit (is_colimit.of_iso_colimit
   (limits.pullback_cone.is_limit_equiv_is_colimit_unop h.flip.cone h.flip.is_limit)
   h.to_comm_sq.flip.cone_unop)
 
+lemma of_vert_is_iso [is_iso snd] [is_iso f] (sq : comm_sq fst snd f g) :
+  is_pullback fst snd f g := is_pullback.flip (of_horiz_is_iso sq.flip)
+
 end is_pullback
 
 namespace is_pushout

src/category_theory/morphism_property.lean

@@ -5,6 +5,7 @@ Authors: Andrew Yang
 -/
 import category_theory.limits.shapes.pullbacks
 import category_theory.arrow
+import category_theory.limits.shapes.comm_sq
 
 /-!
 # Properties of morphisms
@@ -15,7 +16,8 @@ The following meta-properties are defined
 * `respects_iso`: `P` respects isomorphisms if `P f → P (e ≫ f)` and `P f → P (f ≫ e)`, where
   `e` is an isomorphism.
 * `stable_under_composition`: `P` is stable under composition if `P f → P g → P (f ≫ g)`.
-* `stable_under_base_change`: `P` is stable under base change if `P (Y ⟶ S) → P (X ×[S] Y ⟶ X)`.
+* `stable_under_base_change`: `P` is stable under base change if in all pullback
+  squares, the left map satisfies `P` if the right map satisfies it.
 
 -/
 
@@ -56,8 +58,9 @@ def stable_under_inverse (P : morphism_property C) : Prop :=
 
 /-- A morphism property is `stable_under_base_change` if the base change of such a morphism
 still falls in the class. -/
-def stable_under_base_change [has_pullbacks C] (P : morphism_property C) : Prop :=
-∀ ⦃X Y S : C⦄ (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst : pullback f g ⟶ X)
+def stable_under_base_change (P : morphism_property C) : Prop :=
+∀ ⦃X Y Y' S : C⦄ ⦃f : X ⟶ S⦄ ⦃g : Y ⟶ S⦄ ⦃f' : Y' ⟶ Y⦄ ⦃g' : Y' ⟶ X⦄
+  (sq : is_pullback f' g' g f) (hg : P g), P g'
 
 lemma stable_under_composition.respects_iso {P : morphism_property C}
   (hP : stable_under_composition P) (hP' : ∀ {X Y} (e : X ≅ Y), P e.hom) : respects_iso P :=
@@ -82,42 +85,67 @@ lemma respects_iso.arrow_mk_iso_iff {P : morphism_property C}
     P f ↔ P g :=
 hP.arrow_iso_iff e
 
--- This is here to mirror `stable_under_base_change.snd`.
-@[nolint unused_arguments]
-lemma stable_under_base_change.fst [has_pullbacks C] {P : morphism_property C}
-  (hP : stable_under_base_change P) (hP' : respects_iso P) {X Y S : C} (f : X ⟶ S)
-  (g : Y ⟶ S) (H : P g) : P (pullback.fst : pullback f g ⟶ X) :=
-hP f g H
+lemma respects_iso.of_respects_arrow_iso (P : morphism_property C)
+  (hP : ∀ (f g : arrow C) (e : f ≅ g) (hf : P f.hom), P g.hom) : respects_iso P :=
+begin
+  split,
+  { intros X Y Z e f hf,
+    refine hP (arrow.mk f) (arrow.mk (e.hom ≫ f)) (arrow.iso_mk e.symm (iso.refl _) _) hf,
+    dsimp,
+    simp only [iso.inv_hom_id_assoc, category.comp_id], },
+  { intros X Y Z e f hf,
+    refine hP (arrow.mk f) (arrow.mk (f ≫ e.hom)) (arrow.iso_mk (iso.refl _) e _) hf,
+    dsimp,
+    simp only [category.id_comp], },
+end
 
-lemma stable_under_base_change.snd [has_pullbacks C] {P : morphism_property C}
-  (hP : stable_under_base_change P) (hP' : respects_iso P) {X Y S : C} (f : X ⟶ S)
-  (g : Y ⟶ S) (H : P f) : P (pullback.snd : pullback f g ⟶ Y) :=
+lemma stable_under_base_change.mk {P : morphism_property C} [has_pullbacks C]
+  (hP₁ : respects_iso P)
+  (hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) (hg : P g), P (pullback.fst : pullback f g ⟶ X)) :
+  stable_under_base_change P := λ X Y Y' S f g f' g' sq hg,
 begin
-  rw [← pullback_symmetry_hom_comp_fst, hP'.cancel_left_is_iso],
-  exact hP g f H
+  let e := sq.flip.iso_pullback,
+  rw [← hP₁.cancel_left_is_iso e.inv, sq.flip.iso_pullback_inv_fst],
+  exact hP₂ _ _ _ f g hg,
 end
 
+lemma stable_under_base_change.respects_iso {P : morphism_property C}
+  (hP : stable_under_base_change P) : respects_iso P :=
+begin
+  apply respects_iso.of_respects_arrow_iso,
+  intros f g e,
+  exact hP (is_pullback.of_horiz_is_iso (comm_sq.mk e.inv.w)),
+end
+
+lemma stable_under_base_change.fst {P : morphism_property C}
+  (hP : stable_under_base_change P) {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [has_pullback f g]
+  (H : P g) : P (pullback.fst : pullback f g ⟶ X) :=
+hP (is_pullback.of_has_pullback f g).flip H
+
+lemma stable_under_base_change.snd {P : morphism_property C}
+  (hP : stable_under_base_change P) {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [has_pullback f g]
+  (H : P f) : P (pullback.snd : pullback f g ⟶ Y) :=
+hP (is_pullback.of_has_pullback f g) H
+
 lemma stable_under_base_change.base_change_obj [has_pullbacks C] {P : morphism_property C}
-  (hP : stable_under_base_change P) (hP' : respects_iso P) {S S' : C} (f : S' ⟶ S)
+  (hP : stable_under_base_change P) {S S' : C} (f : S' ⟶ S)
   (X : over S) (H : P X.hom) : P ((base_change f).obj X).hom :=
-hP.snd hP' X.hom f H
+hP.snd X.hom f H
 
 lemma stable_under_base_change.base_change_map [has_pullbacks C] {P : morphism_property C}
-  (hP : stable_under_base_change P) (hP' : respects_iso P) {S S' : C} (f : S' ⟶ S)
+  (hP : stable_under_base_change P) {S S' : C} (f : S' ⟶ S)
   {X Y : over S} (g : X ⟶ Y) (H : P g.left) : P ((base_change f).map g).left :=
 begin
   let e := pullback_right_pullback_fst_iso Y.hom f g.left ≪≫
     pullback.congr_hom (g.w.trans (category.comp_id _)) rfl,
   have : e.inv ≫ pullback.snd = ((base_change f).map g).left,
   { apply pullback.hom_ext; dsimp; simp },
-  rw [← this, hP'.cancel_left_is_iso],
-  apply hP.snd hP',
-  exact H
+  rw [← this, hP.respects_iso.cancel_left_is_iso],
+  exact hP.snd _ _ H,
 end
 
 lemma stable_under_base_change.pullback_map [has_pullbacks C] {P : morphism_property C}
-  (hP : stable_under_base_change P) (hP' : respects_iso P)
-  (hP'' : stable_under_composition P) {S X X' Y Y' : C}
+  (hP : stable_under_base_change P) (hP' : stable_under_composition P) {S X X' Y Y' : C}
   {f : X ⟶ S} {g : Y ⟶ S} {f' : X' ⟶ S} {g' : Y' ⟶ S} {i₁ : X ⟶ X'} {i₂ : Y ⟶ Y'}
   (h₁ : P i₁) (h₂ : P i₂) (e₁ : f = i₁ ≫ f') (e₂ : g = i₂ ≫ g') :
     P (pullback.map f g f' g' i₁ i₂ (𝟙 _)
@@ -131,9 +159,9 @@ begin
       ((base_change g').map (over.hom_mk _ e₁.symm : over.mk f ⟶ over.mk f')).left,
   { apply pullback.hom_ext; dsimp; simp },
   rw this,
-  apply hP''; rw hP'.cancel_left_is_iso,
-  exacts [hP.base_change_map hP' _ (over.hom_mk _ e₂.symm : over.mk g ⟶ over.mk g') h₂,
-    hP.base_change_map hP' _ (over.hom_mk _ e₁.symm : over.mk f ⟶ over.mk f') h₁],
+  apply hP'; rw hP.respects_iso.cancel_left_is_iso,
+  exacts [hP.base_change_map _ (over.hom_mk _ e₂.symm : over.mk g ⟶ over.mk g') h₂,
+    hP.base_change_map _ (over.hom_mk _ e₁.symm : over.mk f ⟶ over.mk f') h₁],
 end
 
 /-- If `P : morphism_property C` and `F : C ⥤ D`, then