[Merged by Bors] - feat(CategoryTheory): morphism properties that have the two-out-of-three property

Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

@@ -52,14 +52,14 @@ instance (priority := 900) locallyOfFiniteTypeOfIsOpenImmersion {X Y : Scheme} (
   locallyOfFiniteType_eq.symm ▸ RingHom.finiteType_is_local.affineLocally_of_isOpenImmersion f
 #align algebraic_geometry.locally_of_finite_type_of_is_open_immersion AlgebraicGeometry.locallyOfFiniteTypeOfIsOpenImmersion
 
-theorem locallyOfFiniteType_stableUnderComposition :
-    MorphismProperty.StableUnderComposition @LocallyOfFiniteType :=
-  locallyOfFiniteType_eq.symm ▸ RingHom.finiteType_is_local.affineLocally_stableUnderComposition
-#align algebraic_geometry.locally_of_finite_type_stable_under_composition AlgebraicGeometry.locallyOfFiniteType_stableUnderComposition
+instance locallyOfFiniteType_isStableUnderComposition :
+    MorphismProperty.IsStableUnderComposition @LocallyOfFiniteType :=
+  locallyOfFiniteType_eq.symm ▸ RingHom.finiteType_is_local.affineLocally_isStableUnderComposition
+#align algebraic_geometry.locally_of_finite_type_stable_under_composition AlgebraicGeometry.locallyOfFiniteType_isStableUnderComposition
 
 instance locallyOfFiniteTypeComp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
     [hf : LocallyOfFiniteType f] [hg : LocallyOfFiniteType g] : LocallyOfFiniteType (f ≫ g) :=
-  locallyOfFiniteType_stableUnderComposition f g hf hg
+  MorphismProperty.comp_mem _ f g hf hg
 #align algebraic_geometry.locally_of_finite_type_comp AlgebraicGeometry.locallyOfFiniteTypeComp
 
 theorem locallyOfFiniteTypeOfComp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
@@ -95,4 +95,3 @@ theorem locallyOfFiniteType_respectsIso : MorphismProperty.RespectsIso @LocallyO
 #align algebraic_geometry.locally_of_finite_type_respects_iso AlgebraicGeometry.locallyOfFiniteType_respectsIso
 
 end AlgebraicGeometry
-

Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean

@@ -38,14 +38,16 @@ theorem isOpenImmersion_iff_stalk {f : X ⟶ Y} : IsOpenImmersion f ↔
   · rintro ⟨h₁, h₂⟩; exact IsOpenImmersion.of_stalk_iso f h₁
 #align algebraic_geometry.is_open_immersion_iff_stalk AlgebraicGeometry.isOpenImmersion_iff_stalk
 
-theorem isOpenImmersion_stableUnderComposition :
-    MorphismProperty.StableUnderComposition @IsOpenImmersion := by
-  intro X Y Z f g h₁ h₂; exact LocallyRingedSpace.IsOpenImmersion.comp f g
-#align algebraic_geometry.is_open_immersion_stable_under_composition AlgebraicGeometry.isOpenImmersion_stableUnderComposition
+instance isOpenImmersion_isStableUnderComposition :
+    MorphismProperty.IsStableUnderComposition @IsOpenImmersion where
+  comp_mem f g _ _ := LocallyRingedSpace.IsOpenImmersion.comp f g
+#align algebraic_geometry.is_open_immersion_stable_under_composition AlgebraicGeometry.isOpenImmersion_isStableUnderComposition
 
 theorem isOpenImmersion_respectsIso : MorphismProperty.RespectsIso @IsOpenImmersion := by
-  apply isOpenImmersion_stableUnderComposition.respectsIso
-  intro _ _ _; infer_instance
+  apply MorphismProperty.respectsIso_of_isStableUnderComposition
+  intro _ _ f (hf : IsIso f)
+  have : IsIso f := hf
+  infer_instance
 #align algebraic_geometry.is_open_immersion_respects_iso AlgebraicGeometry.isOpenImmersion_respectsIso
 
 theorem isOpenImmersion_is_local_at_target : PropertyIsLocalAtTarget @IsOpenImmersion := by

Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

@@ -242,9 +242,10 @@ theorem quasiCompact_respectsIso : MorphismProperty.RespectsIso @QuasiCompact :=
     targetAffineLocally_respectsIso QuasiCompact.affineProperty_isLocal.1
 #align algebraic_geometry.quasi_compact_respects_iso AlgebraicGeometry.quasiCompact_respectsIso
 
-theorem quasiCompact_stableUnderComposition :
-    MorphismProperty.StableUnderComposition @QuasiCompact := fun _ _ _ _ _ _ _ => inferInstance
-#align algebraic_geometry.quasi_compact_stable_under_composition AlgebraicGeometry.quasiCompact_stableUnderComposition
+instance quasiCompact_isStableUnderComposition :
+    MorphismProperty.IsStableUnderComposition @QuasiCompact where
+  comp_mem _ _ _ _ := inferInstance
+#align algebraic_geometry.quasi_compact_stable_under_composition AlgebraicGeometry.quasiCompact_isStableUnderComposition
 
 theorem QuasiCompact.affineProperty_stableUnderBaseChange :
     QuasiCompact.affineProperty.StableUnderBaseChange := by

Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

@@ -144,12 +144,12 @@ instance (priority := 900) quasiSeparatedOfMono {X Y : Scheme} (f : X ⟶ Y) [Mo
   ⟨inferInstance⟩
 #align algebraic_geometry.quasi_separated_of_mono AlgebraicGeometry.quasiSeparatedOfMono
 
-theorem quasiSeparated_stableUnderComposition :
-    MorphismProperty.StableUnderComposition @QuasiSeparated :=
+instance quasiSeparated_isStableUnderComposition :
+    MorphismProperty.IsStableUnderComposition @QuasiSeparated :=
   quasiSeparated_eq_diagonal_is_quasiCompact.symm ▸
-    quasiCompact_stableUnderComposition.diagonal quasiCompact_respectsIso
-      quasiCompact_stableUnderBaseChange
-#align algebraic_geometry.quasi_separated_stable_under_composition AlgebraicGeometry.quasiSeparated_stableUnderComposition
+    (MorphismProperty.diagonal_isStableUnderComposition
+        quasiCompact_respectsIso quasiCompact_stableUnderBaseChange)
+#align algebraic_geometry.quasi_separated_stable_under_composition AlgebraicGeometry.quasiSeparated_isStableUnderComposition
 
 theorem quasiSeparated_stableUnderBaseChange :
     MorphismProperty.StableUnderBaseChange @QuasiSeparated :=
@@ -159,7 +159,7 @@ theorem quasiSeparated_stableUnderBaseChange :
 
 instance quasiSeparatedComp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [QuasiSeparated f]
     [QuasiSeparated g] : QuasiSeparated (f ≫ g) :=
-  quasiSeparated_stableUnderComposition f g inferInstance inferInstance
+  MorphismProperty.comp_mem _ f g inferInstance inferInstance
 #align algebraic_geometry.quasi_separated_comp AlgebraicGeometry.quasiSeparatedComp
 
 theorem quasiSeparated_respectsIso : MorphismProperty.RespectsIso @QuasiSeparated :=
@@ -242,7 +242,7 @@ instance {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [QuasiSeparated f] :
 
 instance {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [QuasiSeparated f] [QuasiSeparated g] :
     QuasiSeparated (f ≫ g) :=
-  quasiSeparated_stableUnderComposition f g inferInstance inferInstance
+  MorphismProperty.comp_mem _ f g inferInstance inferInstance
 
 theorem quasiSeparatedSpace_of_quasiSeparated {X Y : Scheme} (f : X ⟶ Y)
     [hY : QuasiSeparatedSpace Y.carrier] [QuasiSeparated f] : QuasiSeparatedSpace X.carrier := by

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

@@ -549,47 +549,47 @@ theorem affineLocally_of_comp
   exact h
 #align ring_hom.property_is_local.affine_locally_of_comp RingHom.PropertyIsLocal.affineLocally_of_comp
 
-theorem affineLocally_stableUnderComposition : (affineLocally @P).StableUnderComposition := by
-  intro X Y S f g hf hg
-  let 𝒰 : ∀ i, ((S.affineCover.pullbackCover (f ≫ g)).obj i).OpenCover := by
-    intro i
-    refine' Scheme.OpenCover.bind _ fun i => Scheme.affineCover _
-    apply Scheme.OpenCover.pushforwardIso _
-      (pullbackRightPullbackFstIso g (S.affineCover.map i) f).hom
-    apply Scheme.Pullback.openCoverOfRight
-    exact (pullback g (S.affineCover.map i)).affineCover
-  -- Porting note: used to be - rw [hP.affine_openCover_iff (f ≫ g) S.affineCover _] - but
-  -- metavariables cause problems in the instance search
-  apply (@affine_openCover_iff _ hP _ _ (f ≫ g) S.affineCover _ ?_ ?_).mpr
-  rotate_left
-  · exact 𝒰
-  · intro i j; dsimp [𝒰] at *; infer_instance
-  · rintro i ⟨j, k⟩
-    dsimp at i j k
-    dsimp only [𝒰, Scheme.OpenCover.bind_map, Scheme.OpenCover.pushforwardIso_obj,
-      Scheme.Pullback.openCoverOfRight_obj, Scheme.OpenCover.pushforwardIso_map,
-      Scheme.Pullback.openCoverOfRight_map, Scheme.OpenCover.bind_obj]
-    rw [Category.assoc, Category.assoc, pullbackRightPullbackFstIso_hom_snd,
-      pullback.lift_snd_assoc, Category.assoc, ← Category.assoc, op_comp, Functor.map_comp]
-    apply hP.StableUnderComposition
-    · -- Porting note: used to be exact _|>. hg i j but that can't find an instance
-      apply hP.affine_openCover_iff _ _ _|>.mp
-      exact hg
-    · delta affineLocally at hf
-      -- Porting note: again strange behavior of TFAE
-      have := (hP.isLocal_sourceAffineLocally.affine_openCover_TFAE f).out 0 3
-      rw [this] at hf
-      -- Porting note: needed to help Lean with this instance (same as above)
-      have : IsOpenImmersion <|
-          ((pullback g (S.affineCover.map i)).affineCover.map j ≫ pullback.fst) :=
-        LocallyRingedSpace.IsOpenImmersion.comp _ _
-      specialize hf ((pullback g (S.affineCover.map i)).affineCover.map j ≫ pullback.fst)
-      -- Porting note: again strange behavior of TFAE
-      have := (hP.affine_openCover_TFAE
-        (pullback.snd : pullback f ((pullback g (S.affineCover.map i)).affineCover.map j ≫
-        pullback.fst) ⟶ _)).out 0 3
-      rw [this] at hf
-      apply hf
-#align ring_hom.property_is_local.affine_locally_stable_under_composition RingHom.PropertyIsLocal.affineLocally_stableUnderComposition
+theorem affineLocally_isStableUnderComposition : (affineLocally @P).IsStableUnderComposition where
+  comp_mem {X Y S} f g hf hg := by
+    let 𝒰 : ∀ i, ((S.affineCover.pullbackCover (f ≫ g)).obj i).OpenCover := by
+      intro i
+      refine' Scheme.OpenCover.bind _ fun i => Scheme.affineCover _
+      apply Scheme.OpenCover.pushforwardIso _
+        (pullbackRightPullbackFstIso g (S.affineCover.map i) f).hom
+      apply Scheme.Pullback.openCoverOfRight
+      exact (pullback g (S.affineCover.map i)).affineCover
+    -- Porting note: used to be - rw [hP.affine_openCover_iff (f ≫ g) S.affineCover _] - but
+    -- metavariables cause problems in the instance search
+    apply (@affine_openCover_iff _ hP _ _ (f ≫ g) S.affineCover _ ?_ ?_).mpr
+    rotate_left
+    · exact 𝒰
+    · intro i j; dsimp [𝒰] at *; infer_instance
+    · rintro i ⟨j, k⟩
+      dsimp at i j k
+      dsimp only [𝒰, Scheme.OpenCover.bind_map, Scheme.OpenCover.pushforwardIso_obj,
+        Scheme.Pullback.openCoverOfRight_obj, Scheme.OpenCover.pushforwardIso_map,
+        Scheme.Pullback.openCoverOfRight_map, Scheme.OpenCover.bind_obj]
+      rw [Category.assoc, Category.assoc, pullbackRightPullbackFstIso_hom_snd,
+        pullback.lift_snd_assoc, Category.assoc, ← Category.assoc, op_comp, Functor.map_comp]
+      apply hP.StableUnderComposition
+      · -- Porting note: used to be exact _|>. hg i j but that can't find an instance
+        apply hP.affine_openCover_iff _ _ _|>.mp
+        exact hg
+      · delta affineLocally at hf
+        -- Porting note: again strange behavior of TFAE
+        have := (hP.isLocal_sourceAffineLocally.affine_openCover_TFAE f).out 0 3
+        rw [this] at hf
+        -- Porting note: needed to help Lean with this instance (same as above)
+        have : IsOpenImmersion <|
+            ((pullback g (S.affineCover.map i)).affineCover.map j ≫ pullback.fst) :=
+          LocallyRingedSpace.IsOpenImmersion.comp _ _
+        specialize hf ((pullback g (S.affineCover.map i)).affineCover.map j ≫ pullback.fst)
+        -- Porting note: again strange behavior of TFAE
+        have := (hP.affine_openCover_TFAE
+          (pullback.snd : pullback f ((pullback g (S.affineCover.map i)).affineCover.map j ≫
+          pullback.fst) ⟶ _)).out 0 3
+        rw [this] at hf
+        apply hf
+#align ring_hom.property_is_local.affine_locally_stable_under_composition RingHom.PropertyIsLocal.affineLocally_isStableUnderComposition
 
 end RingHom.PropertyIsLocal

Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

@@ -54,17 +54,27 @@ theorem universallyClosed_stableUnderBaseChange : StableUnderBaseChange @Univers
   universallyClosed_eq.symm ▸ universally_stableUnderBaseChange (topologically @IsClosedMap)
 #align algebraic_geometry.universally_closed_stable_under_base_change AlgebraicGeometry.universallyClosed_stableUnderBaseChange
 
-theorem universallyClosed_stableUnderComposition : StableUnderComposition @UniversallyClosed := by
+instance isClosedMap_isStableUnderComposition :
+    IsStableUnderComposition (topologically @IsClosedMap) where
+  comp_mem f g hf hg := IsClosedMap.comp (f := f.1.base) (g := g.1.base) hg hf
+
+instance universallyClosed_isStableUnderComposition :
+    IsStableUnderComposition @UniversallyClosed := by
   rw [universallyClosed_eq]
-  exact StableUnderComposition.universally (fun X Y Z f g hf hg =>
-    IsClosedMap.comp (f := f.1.base) (g := g.1.base) hg hf)
-#align algebraic_geometry.universally_closed_stable_under_composition AlgebraicGeometry.universallyClosed_stableUnderComposition
+  infer_instance
+#align algebraic_geometry.universally_closed_stable_under_composition AlgebraicGeometry.universallyClosed_isStableUnderComposition
 
 instance universallyClosedTypeComp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
     [hf : UniversallyClosed f] [hg : UniversallyClosed g] : UniversallyClosed (f ≫ g) :=
-  universallyClosed_stableUnderComposition f g hf hg
+  comp_mem _ _ _ hf hg
 #align algebraic_geometry.universally_closed_type_comp AlgebraicGeometry.universallyClosedTypeComp
 
+theorem topologically_isClosedMap_respectsIso : RespectsIso (topologically @IsClosedMap) := by
+  apply MorphismProperty.respectsIso_of_isStableUnderComposition
+  intro _ _ f hf
+  have : IsIso f := hf
+  exact (TopCat.homeoOfIso (Scheme.forgetToTop.mapIso (asIso f))).isClosedMap
+
 instance universallyClosedFst {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hg : UniversallyClosed g] :
     UniversallyClosed (pullback.fst : pullback f g ⟶ _) :=
   universallyClosed_stableUnderBaseChange.fst f g hg
@@ -83,9 +93,7 @@ theorem morphismRestrict_base {X Y : Scheme} (f : X ⟶ Y) (U : Opens Y.carrier)
 theorem universallyClosed_is_local_at_target : PropertyIsLocalAtTarget @UniversallyClosed := by
   rw [universallyClosed_eq]
   apply universallyIsLocalAtTargetOfMorphismRestrict
-  · exact StableUnderComposition.respectsIso (fun X Y Z f g hf hg =>
-        IsClosedMap.comp (f := f.1.base) (g := g.1.base) hg hf)
-      (fun f => (TopCat.homeoOfIso (Scheme.forgetToTop.mapIso f)).isClosedMap)
+  · exact topologically_isClosedMap_respectsIso
   · intro X Y f ι U hU H
     simp_rw [topologically, morphismRestrict_base] at H
     exact (isClosedMap_iff_isClosedMap_of_iSup_eq_top hU).mpr H

Mathlib/CategoryTheory/Localization/Construction.lean

@@ -231,8 +231,8 @@ morphisms in the localized category if it contains the image of the
 morphisms in the original category, the inverses of the morphisms
 in `W` and if it is stable under composition -/
 theorem morphismProperty_is_top (P : MorphismProperty W.Localization)
-    (hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f))
-    (hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)) (hP₃ : P.StableUnderComposition) :
+    [P.IsStableUnderComposition] (hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f))
+    (hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)) :
     P = ⊤ := by
   funext X Y f
   ext
@@ -251,7 +251,7 @@ theorem morphismProperty_is_top (P : MorphismProperty W.Localization)
     · simpa only [Functor.map_id] using hP₁ (𝟙 X₁.obj)
     · let p' : X₁ ⟶X₂ := p
       rw [show p'.cons g = p' ≫ Quiver.Hom.toPath g by rfl, G.map_comp]
-      refine' hP₃ _ _ hp _
+      refine' P.comp_mem _ _ hp _
       rcases g with (g | ⟨g, hg⟩)
       · apply hP₁
       · apply hP₂
@@ -262,10 +262,9 @@ morphisms in the localized category if it contains the image of the
 morphisms in the original category, if is stable under composition
 and if the property is stable by passing to inverses. -/
 theorem morphismProperty_is_top' (P : MorphismProperty W.Localization)
-    (hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f))
-    (hP₂ : ∀ ⦃X Y : W.Localization⦄ (e : X ≅ Y) (_ : P e.hom), P e.inv)
-    (hP₃ : P.StableUnderComposition) : P = ⊤ :=
-  morphismProperty_is_top P hP₁ (fun _ _ w _ => hP₂ _ (hP₁ w)) hP₃
+    [P.IsStableUnderComposition] (hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f))
+    (hP₂ : ∀ ⦃X Y : W.Localization⦄ (e : X ≅ Y) (_ : P e.hom), P e.inv) : P = ⊤ :=
+  morphismProperty_is_top P hP₁ (fun _ _ w _ => hP₂ _ (hP₁ w))
 #align category_theory.localization.construction.morphism_property_is_top' CategoryTheory.Localization.Construction.morphismProperty_is_top'
 
 namespace NatTransExtension
@@ -301,7 +300,6 @@ def natTransExtension {F₁ F₂ : W.Localization ⥤ D} (τ : W.Q ⋙ F₁ ⟶
     refine' morphismProperty_is_top'
       (MorphismProperty.naturalityProperty (NatTransExtension.app τ))
       _ (MorphismProperty.naturalityProperty.stableUnderInverse _)
-      (MorphismProperty.naturalityProperty.stableUnderComposition _)
     intros X Y f
     dsimp
     simpa only [NatTransExtension.app_eq] using τ.naturality f

Mathlib/CategoryTheory/MorphismProperty/Basic.lean

@@ -98,6 +98,10 @@ def inverseImage (P : MorphismProperty D) (F : C ⥤ D) : MorphismProperty C :=
   P (F.map f)
 #align category_theory.morphism_property.inverse_image CategoryTheory.MorphismProperty.inverseImage
 
+@[simp]
+lemma inverseImage_iff (P : MorphismProperty D) (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) :
+    P.inverseImage F f ↔ P (F.map f) := by rfl
+
 /-- The image (up to isomorphisms) of a `MorphismProperty C` by a functor `C ⥤ D` -/
 def map (P : MorphismProperty C) (F : C ⥤ D) : MorphismProperty D := fun _ _ f =>
   ∃ (X' Y' : C)  (f' : X' ⟶ Y') (_ : P f'), Nonempty (Arrow.mk (F.map f') ≅ Arrow.mk f)