From 33a8d3d2aba33f858c9ae84c35479ebeae92672b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 24 Apr 2024 10:08:35 +0200 Subject: [PATCH 01/15] split MorphismProperty.lean --- Mathlib/CategoryTheory/MorphismProperty.lean | 1038 ----------------- .../MorphismProperty/Basic.lean | 402 +++++++ .../MorphismProperty/Composition.lean | 183 +++ .../MorphismProperty/Concrete.lean | 84 ++ .../MorphismProperty/IsInvertedBy.lean | 174 +++ .../MorphismProperty/Limits.lean | 301 +++++ 6 files changed, 1144 insertions(+), 1038 deletions(-) delete mode 100644 Mathlib/CategoryTheory/MorphismProperty.lean create mode 100644 Mathlib/CategoryTheory/MorphismProperty/Basic.lean create mode 100644 Mathlib/CategoryTheory/MorphismProperty/Composition.lean create mode 100644 Mathlib/CategoryTheory/MorphismProperty/Concrete.lean create mode 100644 Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean create mode 100644 Mathlib/CategoryTheory/MorphismProperty/Limits.lean diff --git a/Mathlib/CategoryTheory/MorphismProperty.lean b/Mathlib/CategoryTheory/MorphismProperty.lean deleted file mode 100644 index 70c631be6b178..0000000000000 --- a/Mathlib/CategoryTheory/MorphismProperty.lean +++ /dev/null @@ -1,1038 +0,0 @@ -/- -Copyright (c) 2022 Andrew Yang. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Andrew Yang --/ -import Mathlib.CategoryTheory.Comma.Arrow -import Mathlib.CategoryTheory.ConcreteCategory.Basic -import Mathlib.CategoryTheory.Limits.Shapes.CommSq -import Mathlib.CategoryTheory.Limits.Shapes.Diagonal - -#align_import category_theory.morphism_property from "leanprover-community/mathlib"@"7f963633766aaa3ebc8253100a5229dd463040c7" - -/-! -# Properties of morphisms - -We provide the basic framework for talking about properties of morphisms. -The following meta-properties are defined - -* `RespectsIso`: `P` respects isomorphisms if `P f → P (e ≫ f)` and `P f → P (f ≫ e)`, where - `e` is an isomorphism. -* `StableUnderComposition`: `P` is stable under composition if `P f → P g → P (f ≫ g)`. -* `StableUnderBaseChange`: `P` is stable under base change if in all pullback - squares, the left map satisfies `P` if the right map satisfies it. -* `StableUnderCobaseChange`: `P` is stable under cobase change if in all pushout - squares, the right map satisfies `P` if the left map satisfies it. - --/ - - -universe w v v' u u' - -open CategoryTheory CategoryTheory.Limits Opposite - -noncomputable section - -namespace CategoryTheory - -variable (C : Type u) [Category.{v} C] {D : Type*} [Category D] - -/-- A `MorphismProperty C` is a class of morphisms between objects in `C`. -/ -def MorphismProperty := - ∀ ⦃X Y : C⦄ (_ : X ⟶ Y), Prop -#align category_theory.morphism_property CategoryTheory.MorphismProperty - -instance : CompleteLattice (MorphismProperty C) := by - dsimp only [MorphismProperty] - infer_instance - -instance : Inhabited (MorphismProperty C) := - ⟨⊤⟩ - -lemma MorphismProperty.top_eq : (⊤ : MorphismProperty C) = fun _ _ _ => True := rfl - -variable {C} - -namespace MorphismProperty - -@[ext] -lemma ext (W W' : MorphismProperty C) (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f) : - W = W' := by - funext X Y f - rw [h] - -lemma top_apply {X Y : C} (f : X ⟶ Y) : (⊤ : MorphismProperty C) f := by - simp only [top_eq] - -instance : HasSubset (MorphismProperty C) := - ⟨fun P₁ P₂ => ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (_ : P₁ f), P₂ f⟩ - -instance : IsTrans (MorphismProperty C) (· ⊆ ·) := - ⟨fun _ _ _ h₁₂ h₂₃ _ _ _ h => h₂₃ _ (h₁₂ _ h)⟩ - -instance : Inter (MorphismProperty C) := - ⟨fun P₁ P₂ _ _ f => P₁ f ∧ P₂ f⟩ - -lemma subset_iff_le (P Q : MorphismProperty C) : P ⊆ Q ↔ P ≤ Q := Iff.rfl - -instance : IsAntisymm (MorphismProperty C) (· ⊆ ·) := - ⟨fun P Q => by simpa only [subset_iff_le] using le_antisymm⟩ - -instance : IsRefl (MorphismProperty C) (· ⊆ ·) := - ⟨fun P => by simpa only [subset_iff_le] using le_refl P⟩ - -/-- The morphism property in `Cᵒᵖ` associated to a morphism property in `C` -/ -@[simp] -def op (P : MorphismProperty C) : MorphismProperty Cᵒᵖ := fun _ _ f => P f.unop -#align category_theory.morphism_property.op CategoryTheory.MorphismProperty.op - -/-- The morphism property in `C` associated to a morphism property in `Cᵒᵖ` -/ -@[simp] -def unop (P : MorphismProperty Cᵒᵖ) : MorphismProperty C := fun _ _ f => P f.op -#align category_theory.morphism_property.unop CategoryTheory.MorphismProperty.unop - -theorem unop_op (P : MorphismProperty C) : P.op.unop = P := - rfl -#align category_theory.morphism_property.unop_op CategoryTheory.MorphismProperty.unop_op - -theorem op_unop (P : MorphismProperty Cᵒᵖ) : P.unop.op = P := - rfl -#align category_theory.morphism_property.op_unop CategoryTheory.MorphismProperty.op_unop - -/-- The inverse image of a `MorphismProperty D` by a functor `C ⥤ D` -/ -def inverseImage (P : MorphismProperty D) (F : C ⥤ D) : MorphismProperty C := fun _ _ f => - P (F.map f) -#align category_theory.morphism_property.inverse_image CategoryTheory.MorphismProperty.inverseImage - -/-- 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) - -lemma map_mem_map (P : MorphismProperty C) (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) (hf : P f) : - (P.map F) (F.map f) := ⟨X, Y, f, hf, ⟨Iso.refl _⟩⟩ - -lemma monotone_map (P Q : MorphismProperty C) (F : C ⥤ D) (h : P ⊆ Q) : - P.map F ⊆ Q.map F := by - intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩ - exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩ - -/-- A morphism property `RespectsIso` if it still holds when composed with an isomorphism -/ -def RespectsIso (P : MorphismProperty C) : Prop := - (∀ {X Y Z} (e : X ≅ Y) (f : Y ⟶ Z), P f → P (e.hom ≫ f)) ∧ - ∀ {X Y Z} (e : Y ≅ Z) (f : X ⟶ Y), P f → P (f ≫ e.hom) -#align category_theory.morphism_property.respects_iso CategoryTheory.MorphismProperty.RespectsIso - -theorem RespectsIso.op {P : MorphismProperty C} (h : RespectsIso P) : RespectsIso P.op := - ⟨fun e f hf => h.2 e.unop f.unop hf, fun e f hf => h.1 e.unop f.unop hf⟩ -#align category_theory.morphism_property.respects_iso.op CategoryTheory.MorphismProperty.RespectsIso.op - -theorem RespectsIso.unop {P : MorphismProperty Cᵒᵖ} (h : RespectsIso P) : RespectsIso P.unop := - ⟨fun e f hf => h.2 e.op f.op hf, fun e f hf => h.1 e.op f.op hf⟩ -#align category_theory.morphism_property.respects_iso.unop CategoryTheory.MorphismProperty.RespectsIso.unop - -/-- The closure by isomorphisms of a `MorphismProperty` -/ -def isoClosure (P : MorphismProperty C) : MorphismProperty C := - fun _ _ f => ∃ (Y₁ Y₂ : C) (f' : Y₁ ⟶ Y₂) (_ : P f'), Nonempty (Arrow.mk f' ≅ Arrow.mk f) - -lemma subset_isoClosure (P : MorphismProperty C) : P ⊆ P.isoClosure := - fun _ _ f hf => ⟨_, _, f, hf, ⟨Iso.refl _⟩⟩ - -lemma isoClosure_respectsIso (P : MorphismProperty C) : - RespectsIso P.isoClosure := - ⟨fun e f ⟨_, _, f', hf', ⟨iso⟩⟩ => - ⟨_, _, f', hf', ⟨Arrow.isoMk (asIso iso.hom.left ≪≫ e.symm) - (asIso iso.hom.right) (by simp)⟩⟩, - fun e f ⟨_, _, f', hf', ⟨iso⟩⟩ => - ⟨_, _, f', hf', ⟨Arrow.isoMk (asIso iso.hom.left) - (asIso iso.hom.right ≪≫ e) (by simp)⟩⟩⟩ - -lemma monotone_isoClosure (P Q : MorphismProperty C) (h : P ⊆ Q) : - P.isoClosure ⊆ Q.isoClosure := by - intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩ - exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩ - -/-- A morphism property is `StableUnderComposition` if the composition of two such morphisms -still falls in the class. -/ -def StableUnderComposition (P : MorphismProperty C) : Prop := - ∀ ⦃X Y Z⦄ (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → P (f ≫ g) -#align category_theory.morphism_property.stable_under_composition CategoryTheory.MorphismProperty.StableUnderComposition - -theorem StableUnderComposition.op {P : MorphismProperty C} (h : StableUnderComposition P) : - StableUnderComposition P.op := fun _ _ _ f g hf hg => h g.unop f.unop hg hf -#align category_theory.morphism_property.stable_under_composition.op CategoryTheory.MorphismProperty.StableUnderComposition.op - -theorem StableUnderComposition.unop {P : MorphismProperty Cᵒᵖ} (h : StableUnderComposition P) : - StableUnderComposition P.unop := fun _ _ _ f g hf hg => h g.op f.op hg hf -#align category_theory.morphism_property.stable_under_composition.unop CategoryTheory.MorphismProperty.StableUnderComposition.unop - -/-- A morphism property is `StableUnderInverse` if the inverse of a morphism satisfying -the property still falls in the class. -/ -def StableUnderInverse (P : MorphismProperty C) : Prop := - ∀ ⦃X Y⦄ (e : X ≅ Y), P e.hom → P e.inv -#align category_theory.morphism_property.stable_under_inverse CategoryTheory.MorphismProperty.StableUnderInverse - -theorem StableUnderInverse.op {P : MorphismProperty C} (h : StableUnderInverse P) : - StableUnderInverse P.op := fun _ _ e he => h e.unop he -#align category_theory.morphism_property.stable_under_inverse.op CategoryTheory.MorphismProperty.StableUnderInverse.op - -theorem StableUnderInverse.unop {P : MorphismProperty Cᵒᵖ} (h : StableUnderInverse P) : - StableUnderInverse P.unop := fun _ _ e he => h e.op he -#align category_theory.morphism_property.stable_under_inverse.unop CategoryTheory.MorphismProperty.StableUnderInverse.unop - -/-- A morphism property is `StableUnderBaseChange` if the base change of such a morphism -still falls in the class. -/ -def StableUnderBaseChange (P : MorphismProperty C) : Prop := - ∀ ⦃X Y Y' S : C⦄ ⦃f : X ⟶ S⦄ ⦃g : Y ⟶ S⦄ ⦃f' : Y' ⟶ Y⦄ ⦃g' : Y' ⟶ X⦄ (_ : IsPullback f' g' g f) - (_ : P g), P g' -#align category_theory.morphism_property.stable_under_base_change CategoryTheory.MorphismProperty.StableUnderBaseChange - -/-- A morphism property is `StableUnderCobaseChange` if the cobase change of such a morphism -still falls in the class. -/ -def StableUnderCobaseChange (P : MorphismProperty C) : Prop := - ∀ ⦃A A' B B' : C⦄ ⦃f : A ⟶ A'⦄ ⦃g : A ⟶ B⦄ ⦃f' : B ⟶ B'⦄ ⦃g' : A' ⟶ B'⦄ (_ : IsPushout g f f' g') - (_ : P f), P f' -#align category_theory.morphism_property.stable_under_cobase_change CategoryTheory.MorphismProperty.StableUnderCobaseChange - -theorem StableUnderComposition.respectsIso {P : MorphismProperty C} (hP : StableUnderComposition P) - (hP' : ∀ {X Y} (e : X ≅ Y), P e.hom) : RespectsIso P := - ⟨fun e _ hf => hP _ _ (hP' e) hf, fun e _ hf => hP _ _ hf (hP' e)⟩ -#align category_theory.morphism_property.stable_under_composition.respects_iso CategoryTheory.MorphismProperty.StableUnderComposition.respectsIso - -theorem RespectsIso.cancel_left_isIso {P : MorphismProperty C} (hP : RespectsIso P) {X Y Z : C} - (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] : P (f ≫ g) ↔ P g := - ⟨fun h => by simpa using hP.1 (asIso f).symm (f ≫ g) h, hP.1 (asIso f) g⟩ -#align category_theory.morphism_property.respects_iso.cancel_left_is_iso CategoryTheory.MorphismProperty.RespectsIso.cancel_left_isIso - -theorem RespectsIso.cancel_right_isIso {P : MorphismProperty C} (hP : RespectsIso P) {X Y Z : C} - (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] : P (f ≫ g) ↔ P f := - ⟨fun h => by simpa using hP.2 (asIso g).symm (f ≫ g) h, hP.2 (asIso g) f⟩ -#align category_theory.morphism_property.respects_iso.cancel_right_is_iso CategoryTheory.MorphismProperty.RespectsIso.cancel_right_isIso - -theorem RespectsIso.arrow_iso_iff {P : MorphismProperty C} (hP : RespectsIso P) {f g : Arrow C} - (e : f ≅ g) : P f.hom ↔ P g.hom := by - rw [← Arrow.inv_left_hom_right e.hom, hP.cancel_left_isIso, hP.cancel_right_isIso] -#align category_theory.morphism_property.respects_iso.arrow_iso_iff CategoryTheory.MorphismProperty.RespectsIso.arrow_iso_iff - -theorem RespectsIso.arrow_mk_iso_iff {P : MorphismProperty C} (hP : RespectsIso P) {W X Y Z : C} - {f : W ⟶ X} {g : Y ⟶ Z} (e : Arrow.mk f ≅ Arrow.mk g) : P f ↔ P g := - hP.arrow_iso_iff e -#align category_theory.morphism_property.respects_iso.arrow_mk_iso_iff CategoryTheory.MorphismProperty.RespectsIso.arrow_mk_iso_iff - -theorem RespectsIso.of_respects_arrow_iso (P : MorphismProperty C) - (hP : ∀ (f g : Arrow C) (_ : f ≅ g) (_ : P f.hom), P g.hom) : RespectsIso P := by - constructor - · intro X Y Z e f hf - refine' hP (Arrow.mk f) (Arrow.mk (e.hom ≫ f)) (Arrow.isoMk e.symm (Iso.refl _) _) hf - dsimp - simp only [Iso.inv_hom_id_assoc, Category.comp_id] - · intro X Y Z e f hf - refine' hP (Arrow.mk f) (Arrow.mk (f ≫ e.hom)) (Arrow.isoMk (Iso.refl _) e _) hf - dsimp - simp only [Category.id_comp] -#align category_theory.morphism_property.respects_iso.of_respects_arrow_iso CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso - -lemma RespectsIso.isoClosure_eq {P : MorphismProperty C} (hP : P.RespectsIso) : - P.isoClosure = P := by - refine' le_antisymm _ (P.subset_isoClosure) - intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩ - exact (hP.arrow_mk_iso_iff e).1 hf' - -@[simp] -lemma isoClosure_isoClosure (P : MorphismProperty C) : - P.isoClosure.isoClosure = P.isoClosure := - P.isoClosure_respectsIso.isoClosure_eq - -theorem StableUnderBaseChange.mk {P : MorphismProperty C} [HasPullbacks C] (hP₁ : RespectsIso P) - (hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) (_ : P g), P (pullback.fst : pullback f g ⟶ X)) : - StableUnderBaseChange P := fun X Y Y' S f g f' g' sq hg => by - let e := sq.flip.isoPullback - rw [← hP₁.cancel_left_isIso e.inv, sq.flip.isoPullback_inv_fst] - exact hP₂ _ _ _ f g hg -#align category_theory.morphism_property.stable_under_base_change.mk CategoryTheory.MorphismProperty.StableUnderBaseChange.mk - -theorem StableUnderBaseChange.respectsIso {P : MorphismProperty C} (hP : StableUnderBaseChange P) : - RespectsIso P := by - apply RespectsIso.of_respects_arrow_iso - intro f g e - exact hP (IsPullback.of_horiz_isIso (CommSq.mk e.inv.w)) -#align category_theory.morphism_property.stable_under_base_change.respects_iso CategoryTheory.MorphismProperty.StableUnderBaseChange.respectsIso - -theorem StableUnderBaseChange.fst {P : MorphismProperty C} (hP : StableUnderBaseChange P) - {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [HasPullback f g] (H : P g) : - P (pullback.fst : pullback f g ⟶ X) := - hP (IsPullback.of_hasPullback f g).flip H -#align category_theory.morphism_property.stable_under_base_change.fst CategoryTheory.MorphismProperty.StableUnderBaseChange.fst - -theorem StableUnderBaseChange.snd {P : MorphismProperty C} (hP : StableUnderBaseChange P) - {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [HasPullback f g] (H : P f) : - P (pullback.snd : pullback f g ⟶ Y) := - hP (IsPullback.of_hasPullback f g) H -#align category_theory.morphism_property.stable_under_base_change.snd CategoryTheory.MorphismProperty.StableUnderBaseChange.snd - -theorem StableUnderBaseChange.baseChange_obj [HasPullbacks C] {P : MorphismProperty C} - (hP : StableUnderBaseChange P) {S S' : C} (f : S' ⟶ S) (X : Over S) (H : P X.hom) : - P ((baseChange f).obj X).hom := - hP.snd X.hom f H -#align category_theory.morphism_property.stable_under_base_change.base_change_obj CategoryTheory.MorphismProperty.StableUnderBaseChange.baseChange_obj - -theorem StableUnderBaseChange.baseChange_map [HasPullbacks C] {P : MorphismProperty C} - (hP : StableUnderBaseChange P) {S S' : C} (f : S' ⟶ S) {X Y : Over S} (g : X ⟶ Y) - (H : P g.left) : P ((baseChange f).map g).left := by - let e := - pullbackRightPullbackFstIso Y.hom f g.left ≪≫ - pullback.congrHom (g.w.trans (Category.comp_id _)) rfl - have : e.inv ≫ pullback.snd = ((baseChange f).map g).left := by - ext <;> dsimp [e] <;> simp - rw [← this, hP.respectsIso.cancel_left_isIso] - exact hP.snd _ _ H -#align category_theory.morphism_property.stable_under_base_change.base_change_map CategoryTheory.MorphismProperty.StableUnderBaseChange.baseChange_map - -theorem StableUnderBaseChange.pullback_map [HasPullbacks C] {P : MorphismProperty C} - (hP : StableUnderBaseChange P) (hP' : StableUnderComposition 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₂ (𝟙 _) ((Category.comp_id _).trans e₁) - ((Category.comp_id _).trans e₂)) := by - have : - pullback.map f g f' g' i₁ i₂ (𝟙 _) ((Category.comp_id _).trans e₁) - ((Category.comp_id _).trans e₂) = - ((pullbackSymmetry _ _).hom ≫ - ((baseChange _).map (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g')).left) ≫ - (pullbackSymmetry _ _).hom ≫ - ((baseChange g').map (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f')).left := - by ext <;> dsimp <;> simp - rw [this] - apply hP' <;> rw [hP.respectsIso.cancel_left_isIso] - exacts [hP.baseChange_map _ (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g') h₂, - hP.baseChange_map _ (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f') h₁] -#align category_theory.morphism_property.stable_under_base_change.pullback_map CategoryTheory.MorphismProperty.StableUnderBaseChange.pullback_map - -theorem StableUnderCobaseChange.mk {P : MorphismProperty C} [HasPushouts C] (hP₁ : RespectsIso P) - (hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) (_ : P f), P (pushout.inr : B ⟶ pushout f g)) : - StableUnderCobaseChange P := fun A A' B B' f g f' g' sq hf => by - let e := sq.flip.isoPushout - rw [← hP₁.cancel_right_isIso _ e.hom, sq.flip.inr_isoPushout_hom] - exact hP₂ _ _ _ f g hf -#align category_theory.morphism_property.stable_under_cobase_change.mk CategoryTheory.MorphismProperty.StableUnderCobaseChange.mk - -theorem StableUnderCobaseChange.respectsIso {P : MorphismProperty C} - (hP : StableUnderCobaseChange P) : RespectsIso P := - RespectsIso.of_respects_arrow_iso _ fun _ _ e => hP (IsPushout.of_horiz_isIso (CommSq.mk e.hom.w)) -#align category_theory.morphism_property.stable_under_cobase_change.respects_iso CategoryTheory.MorphismProperty.StableUnderCobaseChange.respectsIso - -theorem StableUnderCobaseChange.inl {P : MorphismProperty C} (hP : StableUnderCobaseChange P) - {A B A' : C} (f : A ⟶ A') (g : A ⟶ B) [HasPushout f g] (H : P g) : - P (pushout.inl : A' ⟶ pushout f g) := - hP (IsPushout.of_hasPushout f g) H -#align category_theory.morphism_property.stable_under_cobase_change.inl CategoryTheory.MorphismProperty.StableUnderCobaseChange.inl - -theorem StableUnderCobaseChange.inr {P : MorphismProperty C} (hP : StableUnderCobaseChange P) - {A B A' : C} (f : A ⟶ A') (g : A ⟶ B) [HasPushout f g] (H : P f) : - P (pushout.inr : B ⟶ pushout f g) := - hP (IsPushout.of_hasPushout f g).flip H -#align category_theory.morphism_property.stable_under_cobase_change.inr CategoryTheory.MorphismProperty.StableUnderCobaseChange.inr - -theorem StableUnderCobaseChange.op {P : MorphismProperty C} (hP : StableUnderCobaseChange P) : - StableUnderBaseChange P.op := fun _ _ _ _ _ _ _ _ sq hg => hP sq.unop hg -#align category_theory.morphism_property.stable_under_cobase_change.op CategoryTheory.MorphismProperty.StableUnderCobaseChange.op - -theorem StableUnderCobaseChange.unop {P : MorphismProperty Cᵒᵖ} (hP : StableUnderCobaseChange P) : - StableUnderBaseChange P.unop := fun _ _ _ _ _ _ _ _ sq hg => hP sq.op hg -#align category_theory.morphism_property.stable_under_cobase_change.unop CategoryTheory.MorphismProperty.StableUnderCobaseChange.unop - -theorem StableUnderBaseChange.op {P : MorphismProperty C} (hP : StableUnderBaseChange P) : - StableUnderCobaseChange P.op := fun _ _ _ _ _ _ _ _ sq hf => hP sq.unop hf -#align category_theory.morphism_property.stable_under_base_change.op CategoryTheory.MorphismProperty.StableUnderBaseChange.op - -theorem StableUnderBaseChange.unop {P : MorphismProperty Cᵒᵖ} (hP : StableUnderBaseChange P) : - StableUnderCobaseChange P.unop := fun _ _ _ _ _ _ _ _ sq hf => hP sq.op hf -#align category_theory.morphism_property.stable_under_base_change.unop CategoryTheory.MorphismProperty.StableUnderBaseChange.unop - -/-- If `P : MorphismProperty C` and `F : C ⥤ D`, then -`P.IsInvertedBy F` means that all morphisms in `P` are mapped by `F` -to isomorphisms in `D`. -/ -def IsInvertedBy (P : MorphismProperty C) (F : C ⥤ D) : Prop := - ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (_ : P f), IsIso (F.map f) -#align category_theory.morphism_property.is_inverted_by CategoryTheory.MorphismProperty.IsInvertedBy - -namespace IsInvertedBy - -lemma of_subset (P Q : MorphismProperty C) (F : C ⥤ D) (hQ : Q.IsInvertedBy F) (h : P ⊆ Q) : - P.IsInvertedBy F := - fun _ _ _ hf => hQ _ (h _ hf) - -theorem of_comp {C₁ C₂ C₃ : Type*} [Category C₁] [Category C₂] [Category C₃] - (W : MorphismProperty C₁) (F : C₁ ⥤ C₂) (hF : W.IsInvertedBy F) (G : C₂ ⥤ C₃) : - W.IsInvertedBy (F ⋙ G) := fun X Y f hf => by - haveI := hF f hf - dsimp - infer_instance -#align category_theory.morphism_property.is_inverted_by.of_comp CategoryTheory.MorphismProperty.IsInvertedBy.of_comp - -theorem op {W : MorphismProperty C} {L : C ⥤ D} (h : W.IsInvertedBy L) : W.op.IsInvertedBy L.op := - fun X Y f hf => by - haveI := h f.unop hf - dsimp - infer_instance -#align category_theory.morphism_property.is_inverted_by.op CategoryTheory.MorphismProperty.IsInvertedBy.op - -theorem rightOp {W : MorphismProperty C} {L : Cᵒᵖ ⥤ D} (h : W.op.IsInvertedBy L) : - W.IsInvertedBy L.rightOp := fun X Y f hf => by - haveI := h f.op hf - dsimp - infer_instance -#align category_theory.morphism_property.is_inverted_by.right_op CategoryTheory.MorphismProperty.IsInvertedBy.rightOp - -theorem leftOp {W : MorphismProperty C} {L : C ⥤ Dᵒᵖ} (h : W.IsInvertedBy L) : - W.op.IsInvertedBy L.leftOp := fun X Y f hf => by - haveI := h f.unop hf - dsimp - infer_instance -#align category_theory.morphism_property.is_inverted_by.left_op CategoryTheory.MorphismProperty.IsInvertedBy.leftOp - -theorem unop {W : MorphismProperty C} {L : Cᵒᵖ ⥤ Dᵒᵖ} (h : W.op.IsInvertedBy L) : - W.IsInvertedBy L.unop := fun X Y f hf => by - haveI := h f.op hf - dsimp - infer_instance -#align category_theory.morphism_property.is_inverted_by.unop CategoryTheory.MorphismProperty.IsInvertedBy.unop - -end IsInvertedBy - -/-- Given `app : Π X, F₁.obj X ⟶ F₂.obj X` where `F₁` and `F₂` are two functors, -this is the `morphism_property C` satisfied by the morphisms in `C` with respect -to whom `app` is natural. -/ -@[simp] -def naturalityProperty {F₁ F₂ : C ⥤ D} (app : ∀ X, F₁.obj X ⟶ F₂.obj X) : MorphismProperty C := - fun X Y f => F₁.map f ≫ app Y = app X ≫ F₂.map f -#align category_theory.morphism_property.naturality_property CategoryTheory.MorphismProperty.naturalityProperty - -namespace naturalityProperty - -theorem stableUnderComposition {F₁ F₂ : C ⥤ D} (app : ∀ X, F₁.obj X ⟶ F₂.obj X) : - (naturalityProperty app).StableUnderComposition := fun X Y Z f g hf hg => by - simp only [naturalityProperty] at hf hg ⊢ - simp only [Functor.map_comp, Category.assoc, hg] - slice_lhs 1 2 => rw [hf] - rw [Category.assoc] -#align category_theory.morphism_property.naturality_property.is_stable_under_composition CategoryTheory.MorphismProperty.naturalityProperty.stableUnderComposition - -theorem stableUnderInverse {F₁ F₂ : C ⥤ D} (app : ∀ X, F₁.obj X ⟶ F₂.obj X) : - (naturalityProperty app).StableUnderInverse := fun X Y e he => by - simp only [naturalityProperty] at he ⊢ - rw [← cancel_epi (F₁.map e.hom)] - slice_rhs 1 2 => rw [he] - simp only [Category.assoc, ← F₁.map_comp_assoc, ← F₂.map_comp, e.hom_inv_id, Functor.map_id, - Category.id_comp, Category.comp_id] -#align category_theory.morphism_property.naturality_property.is_stable_under_inverse CategoryTheory.MorphismProperty.naturalityProperty.stableUnderInverse - -end naturalityProperty - -theorem RespectsIso.inverseImage {P : MorphismProperty D} (h : RespectsIso P) (F : C ⥤ D) : - RespectsIso (P.inverseImage F) := by - constructor - all_goals - intro X Y Z e f hf - dsimp [MorphismProperty.inverseImage] - rw [F.map_comp] - exacts [h.1 (F.mapIso e) (F.map f) hf, h.2 (F.mapIso e) (F.map f) hf] -#align category_theory.morphism_property.respects_iso.inverse_image CategoryTheory.MorphismProperty.RespectsIso.inverseImage - -theorem StableUnderComposition.inverseImage {P : MorphismProperty D} (h : StableUnderComposition P) - (F : C ⥤ D) : StableUnderComposition (P.inverseImage F) := fun X Y Z f g hf hg => by - simpa only [← F.map_comp] using h (F.map f) (F.map g) hf hg -#align category_theory.morphism_property.stable_under_composition.inverse_image CategoryTheory.MorphismProperty.StableUnderComposition.inverseImage - -variable (C) - -/-- The `MorphismProperty C` satisfied by isomorphisms in `C`. -/ -def isomorphisms : MorphismProperty C := fun _ _ f => IsIso f -#align category_theory.morphism_property.isomorphisms CategoryTheory.MorphismProperty.isomorphisms - -/-- The `MorphismProperty C` satisfied by monomorphisms in `C`. -/ -def monomorphisms : MorphismProperty C := fun _ _ f => Mono f -#align category_theory.morphism_property.monomorphisms CategoryTheory.MorphismProperty.monomorphisms - -/-- The `MorphismProperty C` satisfied by epimorphisms in `C`. -/ -def epimorphisms : MorphismProperty C := fun _ _ f => Epi f -#align category_theory.morphism_property.epimorphisms CategoryTheory.MorphismProperty.epimorphisms - -section - -variable {C} -variable {X Y : C} (f : X ⟶ Y) - -@[simp] -theorem isomorphisms.iff : (isomorphisms C) f ↔ IsIso f := by rfl -#align category_theory.morphism_property.isomorphisms.iff CategoryTheory.MorphismProperty.isomorphisms.iff - -@[simp] -theorem monomorphisms.iff : (monomorphisms C) f ↔ Mono f := by rfl -#align category_theory.morphism_property.monomorphisms.iff CategoryTheory.MorphismProperty.monomorphisms.iff - -@[simp] -theorem epimorphisms.iff : (epimorphisms C) f ↔ Epi f := by rfl -#align category_theory.morphism_property.epimorphisms.iff CategoryTheory.MorphismProperty.epimorphisms.iff - -theorem isomorphisms.infer_property [hf : IsIso f] : (isomorphisms C) f := - hf -#align category_theory.morphism_property.isomorphisms.infer_property CategoryTheory.MorphismProperty.isomorphisms.infer_property - -theorem monomorphisms.infer_property [hf : Mono f] : (monomorphisms C) f := - hf -#align category_theory.morphism_property.monomorphisms.infer_property CategoryTheory.MorphismProperty.monomorphisms.infer_property - -theorem epimorphisms.infer_property [hf : Epi f] : (epimorphisms C) f := - hf -#align category_theory.morphism_property.epimorphisms.infer_property CategoryTheory.MorphismProperty.epimorphisms.infer_property - -end - -theorem RespectsIso.monomorphisms : RespectsIso (monomorphisms C) := by - constructor <;> - · intro X Y Z e f - simp only [monomorphisms.iff] - intro - apply mono_comp -#align category_theory.morphism_property.respects_iso.monomorphisms CategoryTheory.MorphismProperty.RespectsIso.monomorphisms - -theorem RespectsIso.epimorphisms : RespectsIso (epimorphisms C) := by - constructor <;> - · intro X Y Z e f - simp only [epimorphisms.iff] - intro - apply epi_comp -#align category_theory.morphism_property.respects_iso.epimorphisms CategoryTheory.MorphismProperty.RespectsIso.epimorphisms - -theorem RespectsIso.isomorphisms : RespectsIso (isomorphisms C) := by - constructor <;> - · intro X Y Z e f - simp only [isomorphisms.iff] - intro - infer_instance -#align category_theory.morphism_property.respects_iso.isomorphisms CategoryTheory.MorphismProperty.RespectsIso.isomorphisms - -theorem StableUnderComposition.isomorphisms : StableUnderComposition (isomorphisms C) := - fun X Y Z f g hf hg => by - rw [isomorphisms.iff] at hf hg ⊢ - haveI := hf - haveI := hg - infer_instance -#align category_theory.morphism_property.stable_under_composition.isomorphisms CategoryTheory.MorphismProperty.StableUnderComposition.isomorphisms - -theorem StableUnderComposition.monomorphisms : StableUnderComposition (monomorphisms C) := - fun X Y Z f g hf hg => by - rw [monomorphisms.iff] at hf hg ⊢ - haveI := hf - haveI := hg - apply mono_comp -#align category_theory.morphism_property.stable_under_composition.monomorphisms CategoryTheory.MorphismProperty.StableUnderComposition.monomorphisms - -theorem StableUnderComposition.epimorphisms : StableUnderComposition (epimorphisms C) := - fun X Y Z f g hf hg => by - rw [epimorphisms.iff] at hf hg ⊢ - haveI := hf - haveI := hg - apply epi_comp -#align category_theory.morphism_property.stable_under_composition.epimorphisms CategoryTheory.MorphismProperty.StableUnderComposition.epimorphisms - -variable {C} - - --- porting note (#5171): removed @[nolint has_nonempty_instance] -/-- The full subcategory of `C ⥤ D` consisting of functors inverting morphisms in `W` -/ -def FunctorsInverting (W : MorphismProperty C) (D : Type*) [Category D] := - FullSubcategory fun F : C ⥤ D => W.IsInvertedBy F -#align category_theory.morphism_property.functors_inverting CategoryTheory.MorphismProperty.FunctorsInverting - -@[ext] -lemma FunctorsInverting.ext {W : MorphismProperty C} {F₁ F₂ : FunctorsInverting W D} - (h : F₁.obj = F₂.obj) : F₁ = F₂ := by - cases F₁ - cases F₂ - subst h - rfl - -instance (W : MorphismProperty C) (D : Type*) [Category D] : Category (FunctorsInverting W D) := - FullSubcategory.category _ - --- Porting note: add another `@[ext]` lemma --- since `ext` can't see through the definition to use `NatTrans.ext`. --- See https://github.com/leanprover-community/mathlib4/issues/5229 -@[ext] -lemma FunctorsInverting.hom_ext {W : MorphismProperty C} {F₁ F₂ : FunctorsInverting W D} - {α β : F₁ ⟶ F₂} (h : α.app = β.app) : α = β := - NatTrans.ext _ _ h - -/-- A constructor for `W.FunctorsInverting D` -/ -def FunctorsInverting.mk {W : MorphismProperty C} {D : Type*} [Category D] (F : C ⥤ D) - (hF : W.IsInvertedBy F) : W.FunctorsInverting D := - ⟨F, hF⟩ -#align category_theory.morphism_property.functors_inverting.mk CategoryTheory.MorphismProperty.FunctorsInverting.mk - -theorem IsInvertedBy.iff_of_iso (W : MorphismProperty C) {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) : - W.IsInvertedBy F₁ ↔ W.IsInvertedBy F₂ := by - dsimp [IsInvertedBy] - simp only [NatIso.isIso_map_iff e] -#align category_theory.morphism_property.is_inverted_by.iff_of_iso CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso - -@[simp] -lemma IsInvertedBy.isoClosure_iff (W : MorphismProperty C) (F : C ⥤ D) : - W.isoClosure.IsInvertedBy F ↔ W.IsInvertedBy F := by - constructor - · intro h X Y f hf - exact h _ (W.subset_isoClosure _ hf) - · intro h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩ - have : f = e.inv.left ≫ f' ≫ e.hom.right := by - erw [← e.hom.w, ← Arrow.comp_left_assoc, e.inv_hom_id, Category.id_comp] - rfl - simp only [this, F.map_comp] - have := h _ hf' - infer_instance - -@[simp] -lemma IsInvertedBy.iff_comp {C₁ C₂ C₃ : Type*} [Category C₁] [Category C₂] [Category C₃] - (W : MorphismProperty C₁) (F : C₁ ⥤ C₂) (G : C₂ ⥤ C₃) [G.ReflectsIsomorphisms] : - W.IsInvertedBy (F ⋙ G) ↔ W.IsInvertedBy F := by - constructor - · intro h X Y f hf - have : IsIso (G.map (F.map f)) := h _ hf - exact isIso_of_reflects_iso (F.map f) G - · intro hF - exact IsInvertedBy.of_comp W F hF G - -lemma isoClosure_subset_iff (P Q : MorphismProperty C) (hQ : RespectsIso Q) : - P.isoClosure ⊆ Q ↔ P ⊆ Q := by - constructor - · exact P.subset_isoClosure.trans - · intro h - exact (monotone_isoClosure _ _ h).trans (by rw [hQ.isoClosure_eq]) - -lemma map_respectsIso (P : MorphismProperty C) (F : C ⥤ D) : - (P.map F).RespectsIso := by - apply RespectsIso.of_respects_arrow_iso - intro f g e ⟨X', Y', f', hf', ⟨e'⟩⟩ - exact ⟨X', Y', f', hf', ⟨e' ≪≫ e⟩⟩ - -lemma map_subset_iff (P : MorphismProperty C) (F : C ⥤ D) - (Q : MorphismProperty D) (hQ : RespectsIso Q): - P.map F ⊆ Q ↔ ∀ (X Y : C) (f : X ⟶ Y), P f → Q (F.map f) := by - constructor - · intro h X Y f hf - exact h (F.map f) (map_mem_map P F f hf) - · intro h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩ - exact (hQ.arrow_mk_iso_iff e).1 (h _ _ _ hf') - -lemma IsInvertedBy.iff_map_subset_isomorphisms (W : MorphismProperty C) (F : C ⥤ D) : - W.IsInvertedBy F ↔ W.map F ⊆ isomorphisms D := by - rw [map_subset_iff _ _ _ (RespectsIso.isomorphisms D)] - constructor - · intro h X Y f hf - exact h f hf - · intro h X Y f hf - exact h X Y f hf - -@[simp] -lemma map_isoClosure (P : MorphismProperty C) (F : C ⥤ D) : - P.isoClosure.map F = P.map F := by - apply subset_antisymm - · rw [map_subset_iff _ _ _ (P.map_respectsIso F)] - intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩ - exact ⟨_, _, f', hf', ⟨F.mapArrow.mapIso e⟩⟩ - · exact monotone_map _ _ _ (subset_isoClosure P) - -lemma map_id_eq_isoClosure (P : MorphismProperty C) : - P.map (𝟭 _) = P.isoClosure := by - apply subset_antisymm - · rw [map_subset_iff _ _ _ P.isoClosure_respectsIso] - intro X Y f hf - exact P.subset_isoClosure _ hf - · intro X Y f hf - exact hf - -lemma map_id (P : MorphismProperty C) (hP : RespectsIso P) : - P.map (𝟭 _) = P := by - rw [map_id_eq_isoClosure, hP.isoClosure_eq] - -@[simp] -lemma map_map (P : MorphismProperty C) (F : C ⥤ D) {E : Type*} [Category E] (G : D ⥤ E) : - (P.map F).map G = P.map (F ⋙ G) := by - apply subset_antisymm - · rw [map_subset_iff _ _ _ (map_respectsIso _ (F ⋙ G))] - intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩ - exact ⟨X', Y', f', hf', ⟨G.mapArrow.mapIso e⟩⟩ - · rw [map_subset_iff _ _ _ (map_respectsIso _ G)] - intro X Y f hf - exact map_mem_map _ _ _ (map_mem_map _ _ _ hf) - -lemma IsInvertedBy.map_iff {C₁ C₂ C₃ : Type*} [Category C₁] [Category C₂] [Category C₃] - (W : MorphismProperty C₁) (F : C₁ ⥤ C₂) (G : C₂ ⥤ C₃) : - (W.map F).IsInvertedBy G ↔ W.IsInvertedBy (F ⋙ G) := by - simp only [IsInvertedBy.iff_map_subset_isomorphisms, map_map] - -lemma map_eq_of_iso (P : MorphismProperty C) {F G : C ⥤ D} (e : F ≅ G) : - P.map F = P.map G := by - revert F G e - suffices ∀ {F G : C ⥤ D} (_ : F ≅ G), P.map F ⊆ P.map G from - fun F G e => le_antisymm (this e) (this e.symm) - intro F G e X Y f ⟨X', Y', f', hf', ⟨e'⟩⟩ - exact ⟨X', Y', f', hf', ⟨((Functor.mapArrowFunctor _ _).mapIso e.symm).app (Arrow.mk f') ≪≫ e'⟩⟩ - -lemma map_inverseImage_subset (P : MorphismProperty D) (F : C ⥤ D) : - (P.inverseImage F).map F ⊆ P.isoClosure := - fun _ _ _ ⟨_, _, f, hf, ⟨e⟩⟩ => ⟨_, _, F.map f, hf, ⟨e⟩⟩ - -lemma inverseImage_equivalence_inverse_eq_map_functor - (P : MorphismProperty D) (hP : RespectsIso P) (E : C ≌ D) : - P.inverseImage E.functor = P.map E.inverse := by - apply subset_antisymm - · intro X Y f hf - refine' ⟨_, _, _, hf, ⟨_⟩⟩ - exact ((Functor.mapArrowFunctor _ _).mapIso E.unitIso.symm).app (Arrow.mk f) - · rw [map_subset_iff _ _ _ (hP.inverseImage E.functor)] - intro X Y f hf - exact (hP.arrow_mk_iso_iff - (((Functor.mapArrowFunctor _ _).mapIso E.counitIso).app (Arrow.mk f))).2 hf - -lemma inverseImage_equivalence_functor_eq_map_inverse - (Q : MorphismProperty C) (hQ : RespectsIso Q) (E : C ≌ D) : - Q.inverseImage E.inverse = Q.map E.functor := - inverseImage_equivalence_inverse_eq_map_functor Q hQ E.symm - -lemma map_inverseImage_eq_of_isEquivalence - (P : MorphismProperty D) (hP : P.RespectsIso) (F : C ⥤ D) [F.IsEquivalence] : - (P.inverseImage F).map F = P := by - erw [P.inverseImage_equivalence_inverse_eq_map_functor hP F.asEquivalence, map_map, - P.map_eq_of_iso F.asEquivalence.counitIso, map_id _ hP] - -lemma inverseImage_map_eq_of_isEquivalence - (P : MorphismProperty C) (hP : P.RespectsIso) (F : C ⥤ D) [F.IsEquivalence] : - (P.map F).inverseImage F = P := by - erw [((P.map F).inverseImage_equivalence_inverse_eq_map_functor - (P.map_respectsIso F) (F.asEquivalence)), map_map, - P.map_eq_of_iso F.asEquivalence.unitIso.symm, map_id _ hP] - -section Diagonal - -variable [HasPullbacks C] {P : MorphismProperty C} - -/-- For `P : MorphismProperty C`, `P.diagonal` is a morphism property that holds for `f : X ⟶ Y` -whenever `P` holds for `X ⟶ Y xₓ Y`. -/ -def diagonal (P : MorphismProperty C) : MorphismProperty C := fun _ _ f => P (pullback.diagonal f) -#align category_theory.morphism_property.diagonal CategoryTheory.MorphismProperty.diagonal - -theorem diagonal_iff {X Y : C} {f : X ⟶ Y} : P.diagonal f ↔ P (pullback.diagonal f) := - Iff.rfl -#align category_theory.morphism_property.diagonal_iff CategoryTheory.MorphismProperty.diagonal_iff - -theorem RespectsIso.diagonal (hP : P.RespectsIso) : P.diagonal.RespectsIso := by - constructor - · introv H - rwa [diagonal_iff, pullback.diagonal_comp, hP.cancel_left_isIso, hP.cancel_left_isIso, - ← hP.cancel_right_isIso _ - (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) (by simp) (by simp)), - ← pullback.condition, hP.cancel_left_isIso] - · introv H - delta diagonal - rwa [pullback.diagonal_comp, hP.cancel_right_isIso] -#align category_theory.morphism_property.respects_iso.diagonal CategoryTheory.MorphismProperty.RespectsIso.diagonal - -theorem StableUnderComposition.diagonal (hP : StableUnderComposition P) (hP' : RespectsIso P) - (hP'' : StableUnderBaseChange P) : P.diagonal.StableUnderComposition := by - introv X h₁ h₂ - rw [diagonal_iff, pullback.diagonal_comp] - exact hP _ _ h₁ (by simpa [hP'.cancel_left_isIso] using hP''.snd _ _ h₂) -#align category_theory.morphism_property.stable_under_composition.diagonal CategoryTheory.MorphismProperty.StableUnderComposition.diagonal - -theorem StableUnderBaseChange.diagonal (hP : StableUnderBaseChange P) (hP' : RespectsIso P) : - P.diagonal.StableUnderBaseChange := - StableUnderBaseChange.mk hP'.diagonal - (by - introv h - rw [diagonal_iff, diagonal_pullback_fst, hP'.cancel_left_isIso, hP'.cancel_right_isIso] - exact hP.baseChange_map f _ (by simpa)) -#align category_theory.morphism_property.stable_under_base_change.diagonal CategoryTheory.MorphismProperty.StableUnderBaseChange.diagonal - -end Diagonal - -section Universally - -/-- `P.universally` holds for a morphism `f : X ⟶ Y` iff `P` holds for all `X ×[Y] Y' ⟶ Y'`. -/ -def universally (P : MorphismProperty C) : MorphismProperty C := fun X Y f => - ∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y') (_ : IsPullback f' i₁ i₂ f), P f' -#align category_theory.morphism_property.universally CategoryTheory.MorphismProperty.universally - -theorem universally_respectsIso (P : MorphismProperty C) : P.universally.RespectsIso := by - constructor - · intro X Y Z e f hf X' Z' i₁ i₂ f' H - have : IsPullback (𝟙 _) (i₁ ≫ e.hom) i₁ e.inv := - IsPullback.of_horiz_isIso - ⟨by rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]⟩ - exact hf _ _ _ - (by simpa only [Iso.inv_hom_id_assoc, Category.id_comp] using this.paste_horiz H) - · intro X Y Z e f hf X' Z' i₁ i₂ f' H - have : IsPullback (𝟙 _) i₂ (i₂ ≫ e.inv) e.inv := - IsPullback.of_horiz_isIso ⟨Category.id_comp _⟩ - exact hf _ _ _ (by simpa only [Category.assoc, Iso.hom_inv_id, - Category.comp_id, Category.comp_id] using H.paste_horiz this) -#align category_theory.morphism_property.universally_respects_iso CategoryTheory.MorphismProperty.universally_respectsIso - -theorem universally_stableUnderBaseChange (P : MorphismProperty C) : - P.universally.StableUnderBaseChange := fun _ _ _ _ _ _ _ _ H h₁ _ _ _ _ _ H' => - h₁ _ _ _ (H'.paste_vert H.flip) -#align category_theory.morphism_property.universally_stable_under_base_change CategoryTheory.MorphismProperty.universally_stableUnderBaseChange - -theorem StableUnderComposition.universally [HasPullbacks C] {P : MorphismProperty C} - (hP : P.StableUnderComposition) : P.universally.StableUnderComposition := by - intro X Y Z f g hf hg X' Z' i₁ i₂ f' H - have := pullback.lift_fst _ _ (H.w.trans (Category.assoc _ _ _).symm) - rw [← this] at H ⊢ - apply hP _ _ _ (hg _ _ _ <| IsPullback.of_hasPullback _ _) - exact hf _ _ _ (H.of_right (pullback.lift_snd _ _ _) (IsPullback.of_hasPullback i₂ g)) -#align category_theory.morphism_property.stable_under_composition.universally CategoryTheory.MorphismProperty.StableUnderComposition.universally - -theorem universally_le (P : MorphismProperty C) : P.universally ≤ P := by - intro X Y f hf - exact hf (𝟙 _) (𝟙 _) _ (IsPullback.of_vert_isIso ⟨by rw [Category.comp_id, Category.id_comp]⟩) -#align category_theory.morphism_property.universally_le CategoryTheory.MorphismProperty.universally_le - -theorem StableUnderBaseChange.universally_eq {P : MorphismProperty C} - (hP : P.StableUnderBaseChange) : P.universally = P := - P.universally_le.antisymm fun _ _ _ hf _ _ _ _ _ H => hP H.flip hf -#align category_theory.morphism_property.stable_under_base_change.universally_eq CategoryTheory.MorphismProperty.StableUnderBaseChange.universally_eq - -theorem universally_mono : Monotone (universally : MorphismProperty C → MorphismProperty C) := - fun _ _ h _ _ _ h₁ _ _ _ _ _ H => h _ _ _ (h₁ _ _ _ H) -#align category_theory.morphism_property.universally_mono CategoryTheory.MorphismProperty.universally_mono - -end Universally - -section Bijective - -variable [ConcreteCategory C] - -open Function - -attribute [local instance] ConcreteCategory.instFunLike ConcreteCategory.hasCoeToSort - -variable (C) - -/-- Injectiveness (in a concrete category) as a `MorphismProperty` -/ -protected def injective : MorphismProperty C := fun _ _ f => Injective f -#align category_theory.morphism_property.injective CategoryTheory.MorphismProperty.injective - -/-- Surjectiveness (in a concrete category) as a `MorphismProperty` -/ -protected def surjective : MorphismProperty C := fun _ _ f => Surjective f -#align category_theory.morphism_property.surjective CategoryTheory.MorphismProperty.surjective - -/-- Bijectiveness (in a concrete category) as a `MorphismProperty` -/ -protected def bijective : MorphismProperty C := fun _ _ f => Bijective f -#align category_theory.morphism_property.bijective CategoryTheory.MorphismProperty.bijective - -theorem bijective_eq_sup : - MorphismProperty.bijective C = MorphismProperty.injective C ⊓ MorphismProperty.surjective C := - rfl -#align category_theory.morphism_property.bijective_eq_sup CategoryTheory.MorphismProperty.bijective_eq_sup - -theorem injective_stableUnderComposition : (MorphismProperty.injective C).StableUnderComposition := - fun X Y Z f g hf hg => by - delta MorphismProperty.injective - rw [coe_comp] - exact hg.comp hf -#align category_theory.morphism_property.injective_stable_under_composition CategoryTheory.MorphismProperty.injective_stableUnderComposition - -theorem surjective_stableUnderComposition : - (MorphismProperty.surjective C).StableUnderComposition := fun X Y Z f g hf hg => by - delta MorphismProperty.surjective - rw [coe_comp] - exact hg.comp hf -#align category_theory.morphism_property.surjective_stable_under_composition CategoryTheory.MorphismProperty.surjective_stableUnderComposition - -theorem bijective_stableUnderComposition : (MorphismProperty.bijective C).StableUnderComposition := - fun X Y Z f g hf hg => by - delta MorphismProperty.bijective - rw [coe_comp] - exact hg.comp hf -#align category_theory.morphism_property.bijective_stable_under_composition CategoryTheory.MorphismProperty.bijective_stableUnderComposition - -theorem injective_respectsIso : (MorphismProperty.injective C).RespectsIso := - (injective_stableUnderComposition C).respectsIso - (fun e => ((forget C).mapIso e).toEquiv.injective) -#align category_theory.morphism_property.injective_respects_iso CategoryTheory.MorphismProperty.injective_respectsIso - -theorem surjective_respectsIso : (MorphismProperty.surjective C).RespectsIso := - (surjective_stableUnderComposition C).respectsIso - (fun e => ((forget C).mapIso e).toEquiv.surjective) -#align category_theory.morphism_property.surjective_respects_iso CategoryTheory.MorphismProperty.surjective_respectsIso - -theorem bijective_respectsIso : (MorphismProperty.bijective C).RespectsIso := - (bijective_stableUnderComposition C).respectsIso - (fun e => ((forget C).mapIso e).toEquiv.bijective) -#align category_theory.morphism_property.bijective_respects_iso CategoryTheory.MorphismProperty.bijective_respectsIso - -end Bijective - -/-- Typeclass expressing that a morphism property contain identities. -/ -class ContainsIdentities (W : MorphismProperty C) : Prop := - /-- for all `X : C`, the identity of `X` satisfies the morphism property -/ - id_mem' : ∀ (X : C), W (𝟙 X) - -lemma id_mem (W : MorphismProperty C) [W.ContainsIdentities] (X : C) : - W (𝟙 X) := ContainsIdentities.id_mem' X - -namespace ContainsIdentities - -instance op (W : MorphismProperty C) [W.ContainsIdentities] : - W.op.ContainsIdentities := ⟨fun X => W.id_mem X.unop⟩ - -instance unop (W : MorphismProperty Cᵒᵖ) [W.ContainsIdentities] : - W.unop.ContainsIdentities := ⟨fun X => W.id_mem (Opposite.op X)⟩ - -lemma of_op (W : MorphismProperty C) [W.op.ContainsIdentities] : - W.ContainsIdentities := (inferInstance : W.op.unop.ContainsIdentities) - -lemma of_unop (W : MorphismProperty Cᵒᵖ) [W.unop.ContainsIdentities] : - W.ContainsIdentities := (inferInstance : W.unop.op.ContainsIdentities) - -end ContainsIdentities - -/-- A morphism property is multiplicative if it contains identities and is stable by -composition. -/ -class IsMultiplicative (W : MorphismProperty C) extends W.ContainsIdentities : Prop := - /-- compatibility of -/ - stableUnderComposition : W.StableUnderComposition - -lemma comp_mem (W : MorphismProperty C) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : W f) (hg : W g) - [IsMultiplicative W] : W (f ≫ g) := - IsMultiplicative.stableUnderComposition f g hf hg - -namespace IsMultiplicative - -instance op (W : MorphismProperty C) [IsMultiplicative W] : IsMultiplicative W.op where - stableUnderComposition := fun _ _ _ f g hf hg => W.comp_mem g.unop f.unop hg hf - -instance unop (W : MorphismProperty Cᵒᵖ) [IsMultiplicative W] : IsMultiplicative W.unop where - id_mem' _ := W.id_mem _ - stableUnderComposition := fun _ _ _ f g hf hg => W.comp_mem g.op f.op hg hf - -lemma of_op (W : MorphismProperty C) [IsMultiplicative W.op] : IsMultiplicative W := - (inferInstance : IsMultiplicative W.op.unop) - -lemma of_unop (W : MorphismProperty Cᵒᵖ) [IsMultiplicative W.unop] : IsMultiplicative W := - (inferInstance : IsMultiplicative W.unop.op) - -end IsMultiplicative - -section - -variable {C₁ C₂ : Type*} [Category C₁] [Category C₂] - -/-- If `W₁` and `W₂` are morphism properties on two categories `C₁` and `C₂`, -this is the induced morphism property on `C₁ × C₂`. -/ -def prod (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) : - MorphismProperty (C₁ × C₂) := - fun _ _ f => W₁ f.1 ∧ W₂ f.2 - -instance Prod.containsIdentities (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) - [W₁.ContainsIdentities] [W₂.ContainsIdentities] : (prod W₁ W₂).ContainsIdentities := - ⟨fun _ => ⟨W₁.id_mem _, W₂.id_mem _⟩⟩ - -lemma IsInvertedBy.prod {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} - {E₁ E₂ : Type*} [Category E₁] [Category E₂] {F₁ : C₁ ⥤ E₁} {F₂ : C₂ ⥤ E₂} - (h₁ : W₁.IsInvertedBy F₁) (h₂ : W₂.IsInvertedBy F₂) : - (W₁.prod W₂).IsInvertedBy (F₁.prod F₂) := fun _ _ f hf => by - rw [isIso_prod_iff] - exact ⟨h₁ _ hf.1, h₂ _ hf.2⟩ - -end - -section - -variable {J : Type w} {C : J → Type u} {D : J → Type u'} - [∀ j, Category.{v} (C j)] [∀ j, Category.{v'} (D j)] - (W : ∀ j, MorphismProperty (C j)) - -/-- If `W j` are morphism properties on categories `C j` for all `j`, this is the -induced morphism property on the category `∀ j, C j`. -/ -def pi : MorphismProperty (∀ j, C j) := fun _ _ f => ∀ j, (W j) (f j) - -instance Pi.containsIdentities [∀ j, (W j).ContainsIdentities] : - (pi W).ContainsIdentities := - ⟨fun _ _ => MorphismProperty.id_mem _ _⟩ - -lemma IsInvertedBy.pi (F : ∀ j, C j ⥤ D j) (hF : ∀ j, (W j).IsInvertedBy (F j)) : - (MorphismProperty.pi W).IsInvertedBy (Functor.pi F) := by - intro _ _ f hf - rw [isIso_pi_iff] - intro j - exact hF j _ (hf j) - -end - -section - -variable (W : MorphismProperty C) - -/-- The morphism property on `J ⥤ C` which is defined objectwise -from `W : MorphismProperty C`. -/ -def functorCategory (J : Type*) [Category J] : MorphismProperty (J ⥤ C) := - fun _ _ f => ∀ (j : J), W (f.app j) - -/-- The property that a morphism property `W` is stable under limits -indexed by a category `J`. -/ -def IsStableUnderLimitsOfShape (J : Type*) [Category J] : Prop := - ∀ (X₁ X₂ : J ⥤ C) (c₁ : Cone X₁) (c₂ : Cone X₂) - (_ : IsLimit c₁) (h₂ : IsLimit c₂) (f : X₁ ⟶ X₂) (_ : W.functorCategory J f), - W (h₂.lift (Cone.mk _ (c₁.π ≫ f))) - -variable {W} - -lemma IsStableUnderLimitsOfShape.lim_map {J : Type*} [Category J] - (hW : W.IsStableUnderLimitsOfShape J) {X Y : J ⥤ C} - (f : X ⟶ Y) [HasLimitsOfShape J C] (hf : W.functorCategory _ f) : - W (lim.map f) := - hW X Y _ _ (limit.isLimit X) (limit.isLimit Y) f hf - -variable (W) - -/-- The property that a morphism property `W` is stable under products indexed by a type `J`. -/ -abbrev IsStableUnderProductsOfShape (J : Type*) := W.IsStableUnderLimitsOfShape (Discrete J) - -lemma IsStableUnderProductsOfShape.mk (J : Type*) - (hW₀ : W.RespectsIso) [HasProductsOfShape J C] - (hW : ∀ (X₁ X₂ : J → C) (f : ∀ j, X₁ j ⟶ X₂ j) (_ : ∀ (j : J), W (f j)), - W (Pi.map f)) : W.IsStableUnderProductsOfShape J := by - intro X₁ X₂ c₁ c₂ hc₁ hc₂ f hf - let φ := fun j => f.app (Discrete.mk j) - have hf' := hW _ _ φ (fun j => hf (Discrete.mk j)) - refine' (hW₀.arrow_mk_iso_iff _).2 hf' - refine' Arrow.isoMk - (IsLimit.conePointUniqueUpToIso hc₁ (limit.isLimit X₁) ≪≫ (Pi.isoLimit _).symm) - (IsLimit.conePointUniqueUpToIso hc₂ (limit.isLimit X₂) ≪≫ (Pi.isoLimit _).symm) _ - apply limit.hom_ext - rintro ⟨j⟩ - simp - -/-- The condition that a property of morphisms is stable by finite products. -/ -class IsStableUnderFiniteProducts : Prop := - isStableUnderProductsOfShape (J : Type) [Finite J] : W.IsStableUnderProductsOfShape J - -lemma isStableUnderProductsOfShape_of_isStableUnderFiniteProducts - (J : Type) [Finite J] [W.IsStableUnderFiniteProducts] : - W.IsStableUnderProductsOfShape J := - IsStableUnderFiniteProducts.isStableUnderProductsOfShape J - -end - -end MorphismProperty - -namespace NatTrans - -lemma isIso_app_iff_of_iso {F G : C ⥤ D} (α : F ⟶ G) {X Y : C} (e : X ≅ Y) : - IsIso (α.app X) ↔ IsIso (α.app Y) := - MorphismProperty.RespectsIso.arrow_mk_iso_iff (MorphismProperty.RespectsIso.isomorphisms D) - (Arrow.isoMk (F.mapIso e) (G.mapIso e) (by simp)) - -end NatTrans - -end CategoryTheory diff --git a/Mathlib/CategoryTheory/MorphismProperty/Basic.lean b/Mathlib/CategoryTheory/MorphismProperty/Basic.lean new file mode 100644 index 0000000000000..ea9127db921bc --- /dev/null +++ b/Mathlib/CategoryTheory/MorphismProperty/Basic.lean @@ -0,0 +1,402 @@ +/- +Copyright (c) 2022 Andrew Yang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrew Yang +-/ +import Mathlib.CategoryTheory.Comma.Arrow +import Mathlib.CategoryTheory.ConcreteCategory.Basic +import Mathlib.CategoryTheory.Limits.Shapes.CommSq +import Mathlib.CategoryTheory.Limits.Shapes.Diagonal + +#align_import category_theory.morphism_property from "leanprover-community/mathlib"@"7f963633766aaa3ebc8253100a5229dd463040c7" + +/-! +# Properties of morphisms + +We provide the basic framework for talking about properties of morphisms. +The following meta-property is defined + +* `RespectsIso`: `P` respects isomorphisms if `P f → P (e ≫ f)` and `P f → P (f ≫ e)`, where + `e` is an isomorphism. + +-/ + + +universe w v v' u u' + +open CategoryTheory CategoryTheory.Limits Opposite + +noncomputable section + +namespace CategoryTheory + +variable (C : Type u) [Category.{v} C] {D : Type*} [Category D] + +/-- A `MorphismProperty C` is a class of morphisms between objects in `C`. -/ +def MorphismProperty := + ∀ ⦃X Y : C⦄ (_ : X ⟶ Y), Prop +#align category_theory.morphism_property CategoryTheory.MorphismProperty + +instance : CompleteLattice (MorphismProperty C) := by + dsimp only [MorphismProperty] + infer_instance + +instance : Inhabited (MorphismProperty C) := + ⟨⊤⟩ + +lemma MorphismProperty.top_eq : (⊤ : MorphismProperty C) = fun _ _ _ => True := rfl + +variable {C} + +namespace MorphismProperty + +@[ext] +lemma ext (W W' : MorphismProperty C) (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f) : + W = W' := by + funext X Y f + rw [h] + +lemma top_apply {X Y : C} (f : X ⟶ Y) : (⊤ : MorphismProperty C) f := by + simp only [top_eq] + +instance : HasSubset (MorphismProperty C) := + ⟨fun P₁ P₂ => ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (_ : P₁ f), P₂ f⟩ + +instance : IsTrans (MorphismProperty C) (· ⊆ ·) := + ⟨fun _ _ _ h₁₂ h₂₃ _ _ _ h => h₂₃ _ (h₁₂ _ h)⟩ + +instance : Inter (MorphismProperty C) := + ⟨fun P₁ P₂ _ _ f => P₁ f ∧ P₂ f⟩ + +lemma subset_iff_le (P Q : MorphismProperty C) : P ⊆ Q ↔ P ≤ Q := Iff.rfl + +instance : IsAntisymm (MorphismProperty C) (· ⊆ ·) := + ⟨fun P Q => by simpa only [subset_iff_le] using le_antisymm⟩ + +instance : IsRefl (MorphismProperty C) (· ⊆ ·) := + ⟨fun P => by simpa only [subset_iff_le] using le_refl P⟩ + +/-- The morphism property in `Cᵒᵖ` associated to a morphism property in `C` -/ +@[simp] +def op (P : MorphismProperty C) : MorphismProperty Cᵒᵖ := fun _ _ f => P f.unop +#align category_theory.morphism_property.op CategoryTheory.MorphismProperty.op + +/-- The morphism property in `C` associated to a morphism property in `Cᵒᵖ` -/ +@[simp] +def unop (P : MorphismProperty Cᵒᵖ) : MorphismProperty C := fun _ _ f => P f.op +#align category_theory.morphism_property.unop CategoryTheory.MorphismProperty.unop + +theorem unop_op (P : MorphismProperty C) : P.op.unop = P := + rfl +#align category_theory.morphism_property.unop_op CategoryTheory.MorphismProperty.unop_op + +theorem op_unop (P : MorphismProperty Cᵒᵖ) : P.unop.op = P := + rfl +#align category_theory.morphism_property.op_unop CategoryTheory.MorphismProperty.op_unop + +/-- The inverse image of a `MorphismProperty D` by a functor `C ⥤ D` -/ +def inverseImage (P : MorphismProperty D) (F : C ⥤ D) : MorphismProperty C := fun _ _ f => + P (F.map f) +#align category_theory.morphism_property.inverse_image CategoryTheory.MorphismProperty.inverseImage + +/-- 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) + +lemma map_mem_map (P : MorphismProperty C) (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) (hf : P f) : + (P.map F) (F.map f) := ⟨X, Y, f, hf, ⟨Iso.refl _⟩⟩ + +lemma monotone_map (P Q : MorphismProperty C) (F : C ⥤ D) (h : P ⊆ Q) : + P.map F ⊆ Q.map F := by + intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩ + exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩ + +/-- A morphism property `RespectsIso` if it still holds when composed with an isomorphism -/ +def RespectsIso (P : MorphismProperty C) : Prop := + (∀ {X Y Z} (e : X ≅ Y) (f : Y ⟶ Z), P f → P (e.hom ≫ f)) ∧ + ∀ {X Y Z} (e : Y ≅ Z) (f : X ⟶ Y), P f → P (f ≫ e.hom) +#align category_theory.morphism_property.respects_iso CategoryTheory.MorphismProperty.RespectsIso + +theorem RespectsIso.op {P : MorphismProperty C} (h : RespectsIso P) : RespectsIso P.op := + ⟨fun e f hf => h.2 e.unop f.unop hf, fun e f hf => h.1 e.unop f.unop hf⟩ +#align category_theory.morphism_property.respects_iso.op CategoryTheory.MorphismProperty.RespectsIso.op + +theorem RespectsIso.unop {P : MorphismProperty Cᵒᵖ} (h : RespectsIso P) : RespectsIso P.unop := + ⟨fun e f hf => h.2 e.op f.op hf, fun e f hf => h.1 e.op f.op hf⟩ +#align category_theory.morphism_property.respects_iso.unop CategoryTheory.MorphismProperty.RespectsIso.unop + +/-- The closure by isomorphisms of a `MorphismProperty` -/ +def isoClosure (P : MorphismProperty C) : MorphismProperty C := + fun _ _ f => ∃ (Y₁ Y₂ : C) (f' : Y₁ ⟶ Y₂) (_ : P f'), Nonempty (Arrow.mk f' ≅ Arrow.mk f) + +lemma subset_isoClosure (P : MorphismProperty C) : P ⊆ P.isoClosure := + fun _ _ f hf => ⟨_, _, f, hf, ⟨Iso.refl _⟩⟩ + +lemma isoClosure_respectsIso (P : MorphismProperty C) : + RespectsIso P.isoClosure := + ⟨fun e f ⟨_, _, f', hf', ⟨iso⟩⟩ => + ⟨_, _, f', hf', ⟨Arrow.isoMk (asIso iso.hom.left ≪≫ e.symm) + (asIso iso.hom.right) (by simp)⟩⟩, + fun e f ⟨_, _, f', hf', ⟨iso⟩⟩ => + ⟨_, _, f', hf', ⟨Arrow.isoMk (asIso iso.hom.left) + (asIso iso.hom.right ≪≫ e) (by simp)⟩⟩⟩ + +lemma monotone_isoClosure (P Q : MorphismProperty C) (h : P ⊆ Q) : + P.isoClosure ⊆ Q.isoClosure := by + intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩ + exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩ + +theorem RespectsIso.cancel_left_isIso {P : MorphismProperty C} (hP : RespectsIso P) {X Y Z : C} + (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] : P (f ≫ g) ↔ P g := + ⟨fun h => by simpa using hP.1 (asIso f).symm (f ≫ g) h, hP.1 (asIso f) g⟩ +#align category_theory.morphism_property.respects_iso.cancel_left_is_iso CategoryTheory.MorphismProperty.RespectsIso.cancel_left_isIso + +theorem RespectsIso.cancel_right_isIso {P : MorphismProperty C} (hP : RespectsIso P) {X Y Z : C} + (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] : P (f ≫ g) ↔ P f := + ⟨fun h => by simpa using hP.2 (asIso g).symm (f ≫ g) h, hP.2 (asIso g) f⟩ +#align category_theory.morphism_property.respects_iso.cancel_right_is_iso CategoryTheory.MorphismProperty.RespectsIso.cancel_right_isIso + +theorem RespectsIso.arrow_iso_iff {P : MorphismProperty C} (hP : RespectsIso P) {f g : Arrow C} + (e : f ≅ g) : P f.hom ↔ P g.hom := by + rw [← Arrow.inv_left_hom_right e.hom, hP.cancel_left_isIso, hP.cancel_right_isIso] +#align category_theory.morphism_property.respects_iso.arrow_iso_iff CategoryTheory.MorphismProperty.RespectsIso.arrow_iso_iff + +theorem RespectsIso.arrow_mk_iso_iff {P : MorphismProperty C} (hP : RespectsIso P) {W X Y Z : C} + {f : W ⟶ X} {g : Y ⟶ Z} (e : Arrow.mk f ≅ Arrow.mk g) : P f ↔ P g := + hP.arrow_iso_iff e +#align category_theory.morphism_property.respects_iso.arrow_mk_iso_iff CategoryTheory.MorphismProperty.RespectsIso.arrow_mk_iso_iff + +theorem RespectsIso.of_respects_arrow_iso (P : MorphismProperty C) + (hP : ∀ (f g : Arrow C) (_ : f ≅ g) (_ : P f.hom), P g.hom) : RespectsIso P := by + constructor + · intro X Y Z e f hf + refine' hP (Arrow.mk f) (Arrow.mk (e.hom ≫ f)) (Arrow.isoMk e.symm (Iso.refl _) _) hf + dsimp + simp only [Iso.inv_hom_id_assoc, Category.comp_id] + · intro X Y Z e f hf + refine' hP (Arrow.mk f) (Arrow.mk (f ≫ e.hom)) (Arrow.isoMk (Iso.refl _) e _) hf + dsimp + simp only [Category.id_comp] +#align category_theory.morphism_property.respects_iso.of_respects_arrow_iso CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso + +lemma RespectsIso.isoClosure_eq {P : MorphismProperty C} (hP : P.RespectsIso) : + P.isoClosure = P := by + refine' le_antisymm _ (P.subset_isoClosure) + intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩ + exact (hP.arrow_mk_iso_iff e).1 hf' + +@[simp] +lemma isoClosure_isoClosure (P : MorphismProperty C) : + P.isoClosure.isoClosure = P.isoClosure := + P.isoClosure_respectsIso.isoClosure_eq + +lemma isoClosure_subset_iff (P Q : MorphismProperty C) (hQ : RespectsIso Q) : + P.isoClosure ⊆ Q ↔ P ⊆ Q := by + constructor + · exact P.subset_isoClosure.trans + · intro h + exact (monotone_isoClosure _ _ h).trans (by rw [hQ.isoClosure_eq]) + +lemma map_respectsIso (P : MorphismProperty C) (F : C ⥤ D) : + (P.map F).RespectsIso := by + apply RespectsIso.of_respects_arrow_iso + intro f g e ⟨X', Y', f', hf', ⟨e'⟩⟩ + exact ⟨X', Y', f', hf', ⟨e' ≪≫ e⟩⟩ + +lemma map_subset_iff (P : MorphismProperty C) (F : C ⥤ D) + (Q : MorphismProperty D) (hQ : RespectsIso Q): + P.map F ⊆ Q ↔ ∀ (X Y : C) (f : X ⟶ Y), P f → Q (F.map f) := by + constructor + · intro h X Y f hf + exact h (F.map f) (map_mem_map P F f hf) + · intro h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩ + exact (hQ.arrow_mk_iso_iff e).1 (h _ _ _ hf') + +@[simp] +lemma map_isoClosure (P : MorphismProperty C) (F : C ⥤ D) : + P.isoClosure.map F = P.map F := by + apply subset_antisymm + · rw [map_subset_iff _ _ _ (P.map_respectsIso F)] + intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩ + exact ⟨_, _, f', hf', ⟨F.mapArrow.mapIso e⟩⟩ + · exact monotone_map _ _ _ (subset_isoClosure P) + +lemma map_id_eq_isoClosure (P : MorphismProperty C) : + P.map (𝟭 _) = P.isoClosure := by + apply subset_antisymm + · rw [map_subset_iff _ _ _ P.isoClosure_respectsIso] + intro X Y f hf + exact P.subset_isoClosure _ hf + · intro X Y f hf + exact hf + +lemma map_id (P : MorphismProperty C) (hP : RespectsIso P) : + P.map (𝟭 _) = P := by + rw [map_id_eq_isoClosure, hP.isoClosure_eq] + +@[simp] +lemma map_map (P : MorphismProperty C) (F : C ⥤ D) {E : Type*} [Category E] (G : D ⥤ E) : + (P.map F).map G = P.map (F ⋙ G) := by + apply subset_antisymm + · rw [map_subset_iff _ _ _ (map_respectsIso _ (F ⋙ G))] + intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩ + exact ⟨X', Y', f', hf', ⟨G.mapArrow.mapIso e⟩⟩ + · rw [map_subset_iff _ _ _ (map_respectsIso _ G)] + intro X Y f hf + exact map_mem_map _ _ _ (map_mem_map _ _ _ hf) + +theorem RespectsIso.inverseImage {P : MorphismProperty D} (h : RespectsIso P) (F : C ⥤ D) : + RespectsIso (P.inverseImage F) := by + constructor + all_goals + intro X Y Z e f hf + dsimp [MorphismProperty.inverseImage] + rw [F.map_comp] + exacts [h.1 (F.mapIso e) (F.map f) hf, h.2 (F.mapIso e) (F.map f) hf] +#align category_theory.morphism_property.respects_iso.inverse_image CategoryTheory.MorphismProperty.RespectsIso.inverseImage + +lemma map_eq_of_iso (P : MorphismProperty C) {F G : C ⥤ D} (e : F ≅ G) : + P.map F = P.map G := by + revert F G e + suffices ∀ {F G : C ⥤ D} (_ : F ≅ G), P.map F ⊆ P.map G from + fun F G e => le_antisymm (this e) (this e.symm) + intro F G e X Y f ⟨X', Y', f', hf', ⟨e'⟩⟩ + exact ⟨X', Y', f', hf', ⟨((Functor.mapArrowFunctor _ _).mapIso e.symm).app (Arrow.mk f') ≪≫ e'⟩⟩ + +lemma map_inverseImage_subset (P : MorphismProperty D) (F : C ⥤ D) : + (P.inverseImage F).map F ⊆ P.isoClosure := + fun _ _ _ ⟨_, _, f, hf, ⟨e⟩⟩ => ⟨_, _, F.map f, hf, ⟨e⟩⟩ + +lemma inverseImage_equivalence_inverse_eq_map_functor + (P : MorphismProperty D) (hP : RespectsIso P) (E : C ≌ D) : + P.inverseImage E.functor = P.map E.inverse := by + apply subset_antisymm + · intro X Y f hf + refine' ⟨_, _, _, hf, ⟨_⟩⟩ + exact ((Functor.mapArrowFunctor _ _).mapIso E.unitIso.symm).app (Arrow.mk f) + · rw [map_subset_iff _ _ _ (hP.inverseImage E.functor)] + intro X Y f hf + exact (hP.arrow_mk_iso_iff + (((Functor.mapArrowFunctor _ _).mapIso E.counitIso).app (Arrow.mk f))).2 hf + +lemma inverseImage_equivalence_functor_eq_map_inverse + (Q : MorphismProperty C) (hQ : RespectsIso Q) (E : C ≌ D) : + Q.inverseImage E.inverse = Q.map E.functor := + inverseImage_equivalence_inverse_eq_map_functor Q hQ E.symm + +lemma map_inverseImage_eq_of_isEquivalence + (P : MorphismProperty D) (hP : P.RespectsIso) (F : C ⥤ D) [F.IsEquivalence] : + (P.inverseImage F).map F = P := by + erw [P.inverseImage_equivalence_inverse_eq_map_functor hP F.asEquivalence, map_map, + P.map_eq_of_iso F.asEquivalence.counitIso, map_id _ hP] + +lemma inverseImage_map_eq_of_isEquivalence + (P : MorphismProperty C) (hP : P.RespectsIso) (F : C ⥤ D) [F.IsEquivalence] : + (P.map F).inverseImage F = P := by + erw [((P.map F).inverseImage_equivalence_inverse_eq_map_functor + (P.map_respectsIso F) (F.asEquivalence)), map_map, + P.map_eq_of_iso F.asEquivalence.unitIso.symm, map_id _ hP] + + +variable (C) + +/-- The `MorphismProperty C` satisfied by isomorphisms in `C`. -/ +def isomorphisms : MorphismProperty C := fun _ _ f => IsIso f +#align category_theory.morphism_property.isomorphisms CategoryTheory.MorphismProperty.isomorphisms + +/-- The `MorphismProperty C` satisfied by monomorphisms in `C`. -/ +def monomorphisms : MorphismProperty C := fun _ _ f => Mono f +#align category_theory.morphism_property.monomorphisms CategoryTheory.MorphismProperty.monomorphisms + +/-- The `MorphismProperty C` satisfied by epimorphisms in `C`. -/ +def epimorphisms : MorphismProperty C := fun _ _ f => Epi f +#align category_theory.morphism_property.epimorphisms CategoryTheory.MorphismProperty.epimorphisms + +section + +variable {C} +variable {X Y : C} (f : X ⟶ Y) + +@[simp] +theorem isomorphisms.iff : (isomorphisms C) f ↔ IsIso f := by rfl +#align category_theory.morphism_property.isomorphisms.iff CategoryTheory.MorphismProperty.isomorphisms.iff + +@[simp] +theorem monomorphisms.iff : (monomorphisms C) f ↔ Mono f := by rfl +#align category_theory.morphism_property.monomorphisms.iff CategoryTheory.MorphismProperty.monomorphisms.iff + +@[simp] +theorem epimorphisms.iff : (epimorphisms C) f ↔ Epi f := by rfl +#align category_theory.morphism_property.epimorphisms.iff CategoryTheory.MorphismProperty.epimorphisms.iff + +theorem isomorphisms.infer_property [hf : IsIso f] : (isomorphisms C) f := + hf +#align category_theory.morphism_property.isomorphisms.infer_property CategoryTheory.MorphismProperty.isomorphisms.infer_property + +theorem monomorphisms.infer_property [hf : Mono f] : (monomorphisms C) f := + hf +#align category_theory.morphism_property.monomorphisms.infer_property CategoryTheory.MorphismProperty.monomorphisms.infer_property + +theorem epimorphisms.infer_property [hf : Epi f] : (epimorphisms C) f := + hf +#align category_theory.morphism_property.epimorphisms.infer_property CategoryTheory.MorphismProperty.epimorphisms.infer_property + +end + +theorem RespectsIso.monomorphisms : RespectsIso (monomorphisms C) := by + constructor <;> + · intro X Y Z e f + simp only [monomorphisms.iff] + intro + apply mono_comp +#align category_theory.morphism_property.respects_iso.monomorphisms CategoryTheory.MorphismProperty.RespectsIso.monomorphisms + +theorem RespectsIso.epimorphisms : RespectsIso (epimorphisms C) := by + constructor <;> + · intro X Y Z e f + simp only [epimorphisms.iff] + intro + apply epi_comp +#align category_theory.morphism_property.respects_iso.epimorphisms CategoryTheory.MorphismProperty.RespectsIso.epimorphisms + +theorem RespectsIso.isomorphisms : RespectsIso (isomorphisms C) := by + constructor <;> + · intro X Y Z e f + simp only [isomorphisms.iff] + intro + infer_instance +#align category_theory.morphism_property.respects_iso.isomorphisms CategoryTheory.MorphismProperty.RespectsIso.isomorphisms + +/-- If `W₁` and `W₂` are morphism properties on two categories `C₁` and `C₂`, +this is the induced morphism property on `C₁ × C₂`. -/ +def prod {C₁ C₂ : Type*} [Category C₁] [Category C₂] + (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) : + MorphismProperty (C₁ × C₂) := + fun _ _ f => W₁ f.1 ∧ W₂ f.2 + +/-- If `W j` are morphism properties on categories `C j` for all `j`, this is the +induced morphism property on the category `∀ j, C j`. -/ +def pi {J : Type w} {C : J → Type u} [∀ j, Category.{v} (C j)] + (W : ∀ j, MorphismProperty (C j)) : MorphismProperty (∀ j, C j) := + fun _ _ f => ∀ j, (W j) (f j) + +variable {C} + +/-- The morphism property on `J ⥤ C` which is defined objectwise +from `W : MorphismProperty C`. -/ +def functorCategory (W : MorphismProperty C) (J : Type*) [Category J] : + MorphismProperty (J ⥤ C) := + fun _ _ f => ∀ (j : J), W (f.app j) + +end MorphismProperty + +namespace NatTrans + +lemma isIso_app_iff_of_iso {F G : C ⥤ D} (α : F ⟶ G) {X Y : C} (e : X ≅ Y) : + IsIso (α.app X) ↔ IsIso (α.app Y) := + MorphismProperty.RespectsIso.arrow_mk_iso_iff (MorphismProperty.RespectsIso.isomorphisms D) + (Arrow.isoMk (F.mapIso e) (G.mapIso e) (by simp)) + +end NatTrans + +end CategoryTheory diff --git a/Mathlib/CategoryTheory/MorphismProperty/Composition.lean b/Mathlib/CategoryTheory/MorphismProperty/Composition.lean new file mode 100644 index 0000000000000..d761dc8749721 --- /dev/null +++ b/Mathlib/CategoryTheory/MorphismProperty/Composition.lean @@ -0,0 +1,183 @@ +/- +Copyright (c) 2022 Andrew Yang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrew Yang, Joël Riou +-/ +import Mathlib.CategoryTheory.MorphismProperty.Basic + +/-! +# Compatibilities of properties of morphisms with respect to composition + +Given `P : MorphismProperty C`, we define the predicate `P.StableUnderComposition` +which means that `P f → P g → P (f ≫ g)`. We also introduce the type classes +`W.ContainsIdentities` and `W.IsMultiplicative`. + +## TODO +* define the type class of morphism properties that satisfy the 2-out-of-3 property +(which may require transforming `StableUnderComposition` into a type class) + +-/ + + +universe w v v' u u' + +namespace CategoryTheory + +namespace MorphismProperty + +variable {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D] + +/-- Typeclass expressing that a morphism property contain identities. -/ +class ContainsIdentities (W : MorphismProperty C) : Prop := + /-- for all `X : C`, the identity of `X` satisfies the morphism property -/ + id_mem' : ∀ (X : C), W (𝟙 X) + +lemma id_mem (W : MorphismProperty C) [W.ContainsIdentities] (X : C) : + W (𝟙 X) := ContainsIdentities.id_mem' X + +namespace ContainsIdentities + +instance op (W : MorphismProperty C) [W.ContainsIdentities] : + W.op.ContainsIdentities := ⟨fun X => W.id_mem X.unop⟩ + +instance unop (W : MorphismProperty Cᵒᵖ) [W.ContainsIdentities] : + W.unop.ContainsIdentities := ⟨fun X => W.id_mem (Opposite.op X)⟩ + +lemma of_op (W : MorphismProperty C) [W.op.ContainsIdentities] : + W.ContainsIdentities := (inferInstance : W.op.unop.ContainsIdentities) + +lemma of_unop (W : MorphismProperty Cᵒᵖ) [W.unop.ContainsIdentities] : + W.ContainsIdentities := (inferInstance : W.unop.op.ContainsIdentities) + +end ContainsIdentities + +instance Prod.containsIdentities {C₁ C₂ : Type*} [Category C₁] [Category C₂] + (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) + [W₁.ContainsIdentities] [W₂.ContainsIdentities] : (prod W₁ W₂).ContainsIdentities := + ⟨fun _ => ⟨W₁.id_mem _, W₂.id_mem _⟩⟩ + +instance Pi.containsIdentities {J : Type w} {C : J → Type u} + [∀ j, Category.{v} (C j)] (W : ∀ j, MorphismProperty (C j)) [∀ j, (W j).ContainsIdentities] : + (pi W).ContainsIdentities := + ⟨fun _ _ => MorphismProperty.id_mem _ _⟩ + +/-- A morphism property is `StableUnderComposition` if the composition of two such morphisms +still falls in the class. -/ +def StableUnderComposition (P : MorphismProperty C) : Prop := + ∀ ⦃X Y Z⦄ (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → P (f ≫ g) +#align category_theory.morphism_property.stable_under_composition CategoryTheory.MorphismProperty.StableUnderComposition + +theorem StableUnderComposition.op {P : MorphismProperty C} (h : StableUnderComposition P) : + StableUnderComposition P.op := fun _ _ _ f g hf hg => h g.unop f.unop hg hf +#align category_theory.morphism_property.stable_under_composition.op CategoryTheory.MorphismProperty.StableUnderComposition.op + +theorem StableUnderComposition.unop {P : MorphismProperty Cᵒᵖ} (h : StableUnderComposition P) : + StableUnderComposition P.unop := fun _ _ _ f g hf hg => h g.op f.op hg hf +#align category_theory.morphism_property.stable_under_composition.unop CategoryTheory.MorphismProperty.StableUnderComposition.unop + +/-- A morphism property is `StableUnderInverse` if the inverse of a morphism satisfying +the property still falls in the class. -/ +def StableUnderInverse (P : MorphismProperty C) : Prop := + ∀ ⦃X Y⦄ (e : X ≅ Y), P e.hom → P e.inv +#align category_theory.morphism_property.stable_under_inverse CategoryTheory.MorphismProperty.StableUnderInverse + +theorem StableUnderInverse.op {P : MorphismProperty C} (h : StableUnderInverse P) : + StableUnderInverse P.op := fun _ _ e he => h e.unop he +#align category_theory.morphism_property.stable_under_inverse.op CategoryTheory.MorphismProperty.StableUnderInverse.op + +theorem StableUnderInverse.unop {P : MorphismProperty Cᵒᵖ} (h : StableUnderInverse P) : + StableUnderInverse P.unop := fun _ _ e he => h e.op he +#align category_theory.morphism_property.stable_under_inverse.unop CategoryTheory.MorphismProperty.StableUnderInverse.unop + +theorem StableUnderComposition.respectsIso {P : MorphismProperty C} (hP : StableUnderComposition P) + (hP' : ∀ {X Y} (e : X ≅ Y), P e.hom) : RespectsIso P := + ⟨fun e _ hf => hP _ _ (hP' e) hf, fun e _ hf => hP _ _ hf (hP' e)⟩ +#align category_theory.morphism_property.stable_under_composition.respects_iso CategoryTheory.MorphismProperty.StableUnderComposition.respectsIso + +theorem StableUnderComposition.isomorphisms : StableUnderComposition (isomorphisms C) := + fun X Y Z f g hf hg => by + rw [isomorphisms.iff] at hf hg ⊢ + haveI := hf + haveI := hg + infer_instance +#align category_theory.morphism_property.stable_under_composition.isomorphisms CategoryTheory.MorphismProperty.StableUnderComposition.isomorphisms + +theorem StableUnderComposition.monomorphisms : StableUnderComposition (monomorphisms C) := + fun X Y Z f g hf hg => by + rw [monomorphisms.iff] at hf hg ⊢ + haveI := hf + haveI := hg + apply mono_comp +#align category_theory.morphism_property.stable_under_composition.monomorphisms CategoryTheory.MorphismProperty.StableUnderComposition.monomorphisms + +theorem StableUnderComposition.epimorphisms : StableUnderComposition (epimorphisms C) := + fun X Y Z f g hf hg => by + rw [epimorphisms.iff] at hf hg ⊢ + haveI := hf + haveI := hg + apply epi_comp +#align category_theory.morphism_property.stable_under_composition.epimorphisms CategoryTheory.MorphismProperty.StableUnderComposition.epimorphisms + +theorem StableUnderComposition.inverseImage {P : MorphismProperty D} (h : StableUnderComposition P) + (F : C ⥤ D) : StableUnderComposition (P.inverseImage F) := fun X Y Z f g hf hg => by + simpa only [← F.map_comp] using h (F.map f) (F.map g) hf hg +#align category_theory.morphism_property.stable_under_composition.inverse_image CategoryTheory.MorphismProperty.StableUnderComposition.inverseImage + +/-- Given `app : Π X, F₁.obj X ⟶ F₂.obj X` where `F₁` and `F₂` are two functors, +this is the `morphism_property C` satisfied by the morphisms in `C` with respect +to whom `app` is natural. -/ +@[simp] +def naturalityProperty {F₁ F₂ : C ⥤ D} (app : ∀ X, F₁.obj X ⟶ F₂.obj X) : MorphismProperty C := + fun X Y f => F₁.map f ≫ app Y = app X ≫ F₂.map f +#align category_theory.morphism_property.naturality_property CategoryTheory.MorphismProperty.naturalityProperty + +namespace naturalityProperty + +theorem stableUnderComposition {F₁ F₂ : C ⥤ D} (app : ∀ X, F₁.obj X ⟶ F₂.obj X) : + (naturalityProperty app).StableUnderComposition := fun X Y Z f g hf hg => by + simp only [naturalityProperty] at hf hg ⊢ + simp only [Functor.map_comp, Category.assoc, hg] + slice_lhs 1 2 => rw [hf] + rw [Category.assoc] +#align category_theory.morphism_property.naturality_property.is_stable_under_composition CategoryTheory.MorphismProperty.naturalityProperty.stableUnderComposition + +theorem stableUnderInverse {F₁ F₂ : C ⥤ D} (app : ∀ X, F₁.obj X ⟶ F₂.obj X) : + (naturalityProperty app).StableUnderInverse := fun X Y e he => by + simp only [naturalityProperty] at he ⊢ + rw [← cancel_epi (F₁.map e.hom)] + slice_rhs 1 2 => rw [he] + simp only [Category.assoc, ← F₁.map_comp_assoc, ← F₂.map_comp, e.hom_inv_id, Functor.map_id, + Category.id_comp, Category.comp_id] +#align category_theory.morphism_property.naturality_property.is_stable_under_inverse CategoryTheory.MorphismProperty.naturalityProperty.stableUnderInverse + +end naturalityProperty + +/-- A morphism property is multiplicative if it contains identities and is stable by +composition. -/ +class IsMultiplicative (W : MorphismProperty C) extends W.ContainsIdentities : Prop := + stableUnderComposition : W.StableUnderComposition + +lemma comp_mem (W : MorphismProperty C) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : W f) (hg : W g) + [IsMultiplicative W] : W (f ≫ g) := + IsMultiplicative.stableUnderComposition f g hf hg + +namespace IsMultiplicative + +instance op (W : MorphismProperty C) [IsMultiplicative W] : IsMultiplicative W.op where + stableUnderComposition := fun _ _ _ f g hf hg => W.comp_mem g.unop f.unop hg hf + +instance unop (W : MorphismProperty Cᵒᵖ) [IsMultiplicative W] : IsMultiplicative W.unop where + id_mem' _ := W.id_mem _ + stableUnderComposition := fun _ _ _ f g hf hg => W.comp_mem g.op f.op hg hf + +lemma of_op (W : MorphismProperty C) [IsMultiplicative W.op] : IsMultiplicative W := + (inferInstance : IsMultiplicative W.op.unop) + +lemma of_unop (W : MorphismProperty Cᵒᵖ) [IsMultiplicative W.unop] : IsMultiplicative W := + (inferInstance : IsMultiplicative W.unop.op) + +end IsMultiplicative + +end MorphismProperty + +end CategoryTheory diff --git a/Mathlib/CategoryTheory/MorphismProperty/Concrete.lean b/Mathlib/CategoryTheory/MorphismProperty/Concrete.lean new file mode 100644 index 0000000000000..947bed31cbaae --- /dev/null +++ b/Mathlib/CategoryTheory/MorphismProperty/Concrete.lean @@ -0,0 +1,84 @@ +/- +Copyright (c) 2022 Andrew Yang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrew Yang +-/ +import Mathlib.CategoryTheory.MorphismProperty.Composition + +/-! +# Morphism properties defined in concrete categories + +In this file, we define the class of morphisms `MorphismProperty.injective`, +`MorphismProperty.surjective`, `MorphismProperty.bijective` in concrete +categories, and show that it is stable under composition and respect isomorphisms. + +-/ + +universe v u + +namespace CategoryTheory + +namespace MorphismProperty + +variable (C : Type u) [Category.{v} C] [ConcreteCategory C] + +open Function + +attribute [local instance] ConcreteCategory.instFunLike ConcreteCategory.hasCoeToSort + +/-- Injectiveness (in a concrete category) as a `MorphismProperty` -/ +protected def injective : MorphismProperty C := fun _ _ f => Injective f +#align category_theory.morphism_property.injective CategoryTheory.MorphismProperty.injective + +/-- Surjectiveness (in a concrete category) as a `MorphismProperty` -/ +protected def surjective : MorphismProperty C := fun _ _ f => Surjective f +#align category_theory.morphism_property.surjective CategoryTheory.MorphismProperty.surjective + +/-- Bijectiveness (in a concrete category) as a `MorphismProperty` -/ +protected def bijective : MorphismProperty C := fun _ _ f => Bijective f +#align category_theory.morphism_property.bijective CategoryTheory.MorphismProperty.bijective + +theorem bijective_eq_sup : + MorphismProperty.bijective C = MorphismProperty.injective C ⊓ MorphismProperty.surjective C := + rfl +#align category_theory.morphism_property.bijective_eq_sup CategoryTheory.MorphismProperty.bijective_eq_sup + +theorem injective_stableUnderComposition : (MorphismProperty.injective C).StableUnderComposition := + fun X Y Z f g hf hg => by + delta MorphismProperty.injective + rw [coe_comp] + exact hg.comp hf +#align category_theory.morphism_property.injective_stable_under_composition CategoryTheory.MorphismProperty.injective_stableUnderComposition + +theorem surjective_stableUnderComposition : + (MorphismProperty.surjective C).StableUnderComposition := fun X Y Z f g hf hg => by + delta MorphismProperty.surjective + rw [coe_comp] + exact hg.comp hf +#align category_theory.morphism_property.surjective_stable_under_composition CategoryTheory.MorphismProperty.surjective_stableUnderComposition + +theorem bijective_stableUnderComposition : (MorphismProperty.bijective C).StableUnderComposition := + fun X Y Z f g hf hg => by + delta MorphismProperty.bijective + rw [coe_comp] + exact hg.comp hf +#align category_theory.morphism_property.bijective_stable_under_composition CategoryTheory.MorphismProperty.bijective_stableUnderComposition + +theorem injective_respectsIso : (MorphismProperty.injective C).RespectsIso := + (injective_stableUnderComposition C).respectsIso + (fun e => ((forget C).mapIso e).toEquiv.injective) +#align category_theory.morphism_property.injective_respects_iso CategoryTheory.MorphismProperty.injective_respectsIso + +theorem surjective_respectsIso : (MorphismProperty.surjective C).RespectsIso := + (surjective_stableUnderComposition C).respectsIso + (fun e => ((forget C).mapIso e).toEquiv.surjective) +#align category_theory.morphism_property.surjective_respects_iso CategoryTheory.MorphismProperty.surjective_respectsIso + +theorem bijective_respectsIso : (MorphismProperty.bijective C).RespectsIso := + (bijective_stableUnderComposition C).respectsIso + (fun e => ((forget C).mapIso e).toEquiv.bijective) +#align category_theory.morphism_property.bijective_respects_iso CategoryTheory.MorphismProperty.bijective_respectsIso + +end MorphismProperty + +end CategoryTheory diff --git a/Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean b/Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean new file mode 100644 index 0000000000000..fde6405d93e47 --- /dev/null +++ b/Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean @@ -0,0 +1,174 @@ +/- +Copyright (c) 2022 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +import Mathlib.CategoryTheory.MorphismProperty.Basic + +/-! +# Morphism properties that are inverted by a functor + +In this file, we introduce the predicate `P.IsInvertedBy F` which expresses +that the morphisms satisfying `P : MorphismProperty C` are mapped to +isomorphisms by a functor `F : C ⥤ D`. + +This is used in the localization of categories API (folder `CategoryTheory.Localization`). + +-/ + +universe w v v' u u' + +namespace CategoryTheory + +namespace MorphismProperty + +variable {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D] + +/-- If `P : MorphismProperty C` and `F : C ⥤ D`, then +`P.IsInvertedBy F` means that all morphisms in `P` are mapped by `F` +to isomorphisms in `D`. -/ +def IsInvertedBy (P : MorphismProperty C) (F : C ⥤ D) : Prop := + ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (_ : P f), IsIso (F.map f) +#align category_theory.morphism_property.is_inverted_by CategoryTheory.MorphismProperty.IsInvertedBy + +namespace IsInvertedBy + +lemma of_subset (P Q : MorphismProperty C) (F : C ⥤ D) (hQ : Q.IsInvertedBy F) (h : P ⊆ Q) : + P.IsInvertedBy F := + fun _ _ _ hf => hQ _ (h _ hf) + +theorem of_comp {C₁ C₂ C₃ : Type*} [Category C₁] [Category C₂] [Category C₃] + (W : MorphismProperty C₁) (F : C₁ ⥤ C₂) (hF : W.IsInvertedBy F) (G : C₂ ⥤ C₃) : + W.IsInvertedBy (F ⋙ G) := fun X Y f hf => by + haveI := hF f hf + dsimp + infer_instance +#align category_theory.morphism_property.is_inverted_by.of_comp CategoryTheory.MorphismProperty.IsInvertedBy.of_comp + +theorem op {W : MorphismProperty C} {L : C ⥤ D} (h : W.IsInvertedBy L) : W.op.IsInvertedBy L.op := + fun X Y f hf => by + haveI := h f.unop hf + dsimp + infer_instance +#align category_theory.morphism_property.is_inverted_by.op CategoryTheory.MorphismProperty.IsInvertedBy.op + +theorem rightOp {W : MorphismProperty C} {L : Cᵒᵖ ⥤ D} (h : W.op.IsInvertedBy L) : + W.IsInvertedBy L.rightOp := fun X Y f hf => by + haveI := h f.op hf + dsimp + infer_instance +#align category_theory.morphism_property.is_inverted_by.right_op CategoryTheory.MorphismProperty.IsInvertedBy.rightOp + +theorem leftOp {W : MorphismProperty C} {L : C ⥤ Dᵒᵖ} (h : W.IsInvertedBy L) : + W.op.IsInvertedBy L.leftOp := fun X Y f hf => by + haveI := h f.unop hf + dsimp + infer_instance +#align category_theory.morphism_property.is_inverted_by.left_op CategoryTheory.MorphismProperty.IsInvertedBy.leftOp + +theorem unop {W : MorphismProperty C} {L : Cᵒᵖ ⥤ Dᵒᵖ} (h : W.op.IsInvertedBy L) : + W.IsInvertedBy L.unop := fun X Y f hf => by + haveI := h f.op hf + dsimp + infer_instance +#align category_theory.morphism_property.is_inverted_by.unop CategoryTheory.MorphismProperty.IsInvertedBy.unop + +lemma prod {C₁ C₂ : Type*} [Category C₁] [Category C₂] + {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} + {E₁ E₂ : Type*} [Category E₁] [Category E₂] {F₁ : C₁ ⥤ E₁} {F₂ : C₂ ⥤ E₂} + (h₁ : W₁.IsInvertedBy F₁) (h₂ : W₂.IsInvertedBy F₂) : + (W₁.prod W₂).IsInvertedBy (F₁.prod F₂) := fun _ _ f hf => by + rw [isIso_prod_iff] + exact ⟨h₁ _ hf.1, h₂ _ hf.2⟩ + +lemma pi {J : Type w} {C : J → Type u} {D : J → Type u'} + [∀ j, Category.{v} (C j)] [∀ j, Category.{v'} (D j)] + (W : ∀ j, MorphismProperty (C j)) (F : ∀ j, C j ⥤ D j) + (hF : ∀ j, (W j).IsInvertedBy (F j)) : + (MorphismProperty.pi W).IsInvertedBy (Functor.pi F) := by + intro _ _ f hf + rw [isIso_pi_iff] + intro j + exact hF j _ (hf j) + +end IsInvertedBy + +-- porting note (#5171): removed @[nolint has_nonempty_instance] +/-- The full subcategory of `C ⥤ D` consisting of functors inverting morphisms in `W` -/ +def FunctorsInverting (W : MorphismProperty C) (D : Type*) [Category D] := + FullSubcategory fun F : C ⥤ D => W.IsInvertedBy F +#align category_theory.morphism_property.functors_inverting CategoryTheory.MorphismProperty.FunctorsInverting + +@[ext] +lemma FunctorsInverting.ext {W : MorphismProperty C} {F₁ F₂ : FunctorsInverting W D} + (h : F₁.obj = F₂.obj) : F₁ = F₂ := by + cases F₁ + cases F₂ + subst h + rfl + +instance (W : MorphismProperty C) (D : Type*) [Category D] : Category (FunctorsInverting W D) := + FullSubcategory.category _ + +-- Porting note: add another `@[ext]` lemma +-- since `ext` can't see through the definition to use `NatTrans.ext`. +-- See https://github.com/leanprover-community/mathlib4/issues/5229 +@[ext] +lemma FunctorsInverting.hom_ext {W : MorphismProperty C} {F₁ F₂ : FunctorsInverting W D} + {α β : F₁ ⟶ F₂} (h : α.app = β.app) : α = β := + NatTrans.ext _ _ h + +/-- A constructor for `W.FunctorsInverting D` -/ +def FunctorsInverting.mk {W : MorphismProperty C} {D : Type*} [Category D] (F : C ⥤ D) + (hF : W.IsInvertedBy F) : W.FunctorsInverting D := + ⟨F, hF⟩ +#align category_theory.morphism_property.functors_inverting.mk CategoryTheory.MorphismProperty.FunctorsInverting.mk + +theorem IsInvertedBy.iff_of_iso (W : MorphismProperty C) {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) : + W.IsInvertedBy F₁ ↔ W.IsInvertedBy F₂ := by + dsimp [IsInvertedBy] + simp only [NatIso.isIso_map_iff e] +#align category_theory.morphism_property.is_inverted_by.iff_of_iso CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso + +@[simp] +lemma IsInvertedBy.isoClosure_iff (W : MorphismProperty C) (F : C ⥤ D) : + W.isoClosure.IsInvertedBy F ↔ W.IsInvertedBy F := by + constructor + · intro h X Y f hf + exact h _ (W.subset_isoClosure _ hf) + · intro h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩ + have : f = e.inv.left ≫ f' ≫ e.hom.right := by + erw [← e.hom.w, ← Arrow.comp_left_assoc, e.inv_hom_id, Category.id_comp] + rfl + simp only [this, F.map_comp] + have := h _ hf' + infer_instance + +@[simp] +lemma IsInvertedBy.iff_comp {C₁ C₂ C₃ : Type*} [Category C₁] [Category C₂] [Category C₃] + (W : MorphismProperty C₁) (F : C₁ ⥤ C₂) (G : C₂ ⥤ C₃) [G.ReflectsIsomorphisms] : + W.IsInvertedBy (F ⋙ G) ↔ W.IsInvertedBy F := by + constructor + · intro h X Y f hf + have : IsIso (G.map (F.map f)) := h _ hf + exact isIso_of_reflects_iso (F.map f) G + · intro hF + exact IsInvertedBy.of_comp W F hF G + +lemma IsInvertedBy.iff_map_subset_isomorphisms (W : MorphismProperty C) (F : C ⥤ D) : + W.IsInvertedBy F ↔ W.map F ⊆ isomorphisms D := by + rw [map_subset_iff _ _ _ (RespectsIso.isomorphisms D)] + constructor + · intro h X Y f hf + exact h f hf + · intro h X Y f hf + exact h X Y f hf + +lemma IsInvertedBy.map_iff {C₁ C₂ C₃ : Type*} [Category C₁] [Category C₂] [Category C₃] + (W : MorphismProperty C₁) (F : C₁ ⥤ C₂) (G : C₂ ⥤ C₃) : + (W.map F).IsInvertedBy G ↔ W.IsInvertedBy (F ⋙ G) := by + simp only [IsInvertedBy.iff_map_subset_isomorphisms, map_map] + +end MorphismProperty + +end CategoryTheory diff --git a/Mathlib/CategoryTheory/MorphismProperty/Limits.lean b/Mathlib/CategoryTheory/MorphismProperty/Limits.lean new file mode 100644 index 0000000000000..1971ab46fb994 --- /dev/null +++ b/Mathlib/CategoryTheory/MorphismProperty/Limits.lean @@ -0,0 +1,301 @@ +/- +Copyright (c) 2022 Andrew Yang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrew Yang, Joël Riou +-/ +import Mathlib.CategoryTheory.MorphismProperty.Composition + +/-! +# Relation of morphism properties with limits + +The following predicates are introduces for morphism properties `P`: +* `StableUnderBaseChange`: `P` is stable under base change if in all pullback + squares, the left map satisfies `P` if the right map satisfies it. +* `StableUnderCobaseChange`: `P` is stable under cobase change if in all pushout + squares, the right map satisfies `P` if the left map satisfies it. + +We define `P.universally` for the class of morphisms which satisfy `P` after any base change. + +We also introduce properties `IsStableUnderProductsOfShape`, `IsStableUnderLimitsOfShape`, +`IsStableUnderFiniteProducts`. + +-/ + +universe v u + +namespace CategoryTheory + +open Limits + +namespace MorphismProperty + +variable {C : Type u} [Category.{v} C] + +/-- A morphism property is `StableUnderBaseChange` if the base change of such a morphism +still falls in the class. -/ +def StableUnderBaseChange (P : MorphismProperty C) : Prop := + ∀ ⦃X Y Y' S : C⦄ ⦃f : X ⟶ S⦄ ⦃g : Y ⟶ S⦄ ⦃f' : Y' ⟶ Y⦄ ⦃g' : Y' ⟶ X⦄ (_ : IsPullback f' g' g f) + (_ : P g), P g' +#align category_theory.morphism_property.stable_under_base_change CategoryTheory.MorphismProperty.StableUnderBaseChange + +/-- A morphism property is `StableUnderCobaseChange` if the cobase change of such a morphism +still falls in the class. -/ +def StableUnderCobaseChange (P : MorphismProperty C) : Prop := + ∀ ⦃A A' B B' : C⦄ ⦃f : A ⟶ A'⦄ ⦃g : A ⟶ B⦄ ⦃f' : B ⟶ B'⦄ ⦃g' : A' ⟶ B'⦄ (_ : IsPushout g f f' g') + (_ : P f), P f' +#align category_theory.morphism_property.stable_under_cobase_change CategoryTheory.MorphismProperty.StableUnderCobaseChange + +theorem StableUnderBaseChange.mk {P : MorphismProperty C} [HasPullbacks C] (hP₁ : RespectsIso P) + (hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) (_ : P g), P (pullback.fst : pullback f g ⟶ X)) : + StableUnderBaseChange P := fun X Y Y' S f g f' g' sq hg => by + let e := sq.flip.isoPullback + rw [← hP₁.cancel_left_isIso e.inv, sq.flip.isoPullback_inv_fst] + exact hP₂ _ _ _ f g hg +#align category_theory.morphism_property.stable_under_base_change.mk CategoryTheory.MorphismProperty.StableUnderBaseChange.mk + +theorem StableUnderBaseChange.respectsIso {P : MorphismProperty C} (hP : StableUnderBaseChange P) : + RespectsIso P := by + apply RespectsIso.of_respects_arrow_iso + intro f g e + exact hP (IsPullback.of_horiz_isIso (CommSq.mk e.inv.w)) +#align category_theory.morphism_property.stable_under_base_change.respects_iso CategoryTheory.MorphismProperty.StableUnderBaseChange.respectsIso + +theorem StableUnderBaseChange.fst {P : MorphismProperty C} (hP : StableUnderBaseChange P) + {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [HasPullback f g] (H : P g) : + P (pullback.fst : pullback f g ⟶ X) := + hP (IsPullback.of_hasPullback f g).flip H +#align category_theory.morphism_property.stable_under_base_change.fst CategoryTheory.MorphismProperty.StableUnderBaseChange.fst + +theorem StableUnderBaseChange.snd {P : MorphismProperty C} (hP : StableUnderBaseChange P) + {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [HasPullback f g] (H : P f) : + P (pullback.snd : pullback f g ⟶ Y) := + hP (IsPullback.of_hasPullback f g) H +#align category_theory.morphism_property.stable_under_base_change.snd CategoryTheory.MorphismProperty.StableUnderBaseChange.snd + +theorem StableUnderBaseChange.baseChange_obj [HasPullbacks C] {P : MorphismProperty C} + (hP : StableUnderBaseChange P) {S S' : C} (f : S' ⟶ S) (X : Over S) (H : P X.hom) : + P ((baseChange f).obj X).hom := + hP.snd X.hom f H +#align category_theory.morphism_property.stable_under_base_change.base_change_obj CategoryTheory.MorphismProperty.StableUnderBaseChange.baseChange_obj + +theorem StableUnderBaseChange.baseChange_map [HasPullbacks C] {P : MorphismProperty C} + (hP : StableUnderBaseChange P) {S S' : C} (f : S' ⟶ S) {X Y : Over S} (g : X ⟶ Y) + (H : P g.left) : P ((baseChange f).map g).left := by + let e := + pullbackRightPullbackFstIso Y.hom f g.left ≪≫ + pullback.congrHom (g.w.trans (Category.comp_id _)) rfl + have : e.inv ≫ pullback.snd = ((baseChange f).map g).left := by + ext <;> dsimp [e] <;> simp + rw [← this, hP.respectsIso.cancel_left_isIso] + exact hP.snd _ _ H +#align category_theory.morphism_property.stable_under_base_change.base_change_map CategoryTheory.MorphismProperty.StableUnderBaseChange.baseChange_map + +theorem StableUnderBaseChange.pullback_map [HasPullbacks C] {P : MorphismProperty C} + (hP : StableUnderBaseChange P) (hP' : StableUnderComposition 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₂ (𝟙 _) ((Category.comp_id _).trans e₁) + ((Category.comp_id _).trans e₂)) := by + have : + pullback.map f g f' g' i₁ i₂ (𝟙 _) ((Category.comp_id _).trans e₁) + ((Category.comp_id _).trans e₂) = + ((pullbackSymmetry _ _).hom ≫ + ((baseChange _).map (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g')).left) ≫ + (pullbackSymmetry _ _).hom ≫ + ((baseChange g').map (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f')).left := + by ext <;> dsimp <;> simp + rw [this] + apply hP' <;> rw [hP.respectsIso.cancel_left_isIso] + exacts [hP.baseChange_map _ (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g') h₂, + hP.baseChange_map _ (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f') h₁] +#align category_theory.morphism_property.stable_under_base_change.pullback_map CategoryTheory.MorphismProperty.StableUnderBaseChange.pullback_map + +theorem StableUnderCobaseChange.mk {P : MorphismProperty C} [HasPushouts C] (hP₁ : RespectsIso P) + (hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) (_ : P f), P (pushout.inr : B ⟶ pushout f g)) : + StableUnderCobaseChange P := fun A A' B B' f g f' g' sq hf => by + let e := sq.flip.isoPushout + rw [← hP₁.cancel_right_isIso _ e.hom, sq.flip.inr_isoPushout_hom] + exact hP₂ _ _ _ f g hf +#align category_theory.morphism_property.stable_under_cobase_change.mk CategoryTheory.MorphismProperty.StableUnderCobaseChange.mk + +theorem StableUnderCobaseChange.respectsIso {P : MorphismProperty C} + (hP : StableUnderCobaseChange P) : RespectsIso P := + RespectsIso.of_respects_arrow_iso _ fun _ _ e => hP (IsPushout.of_horiz_isIso (CommSq.mk e.hom.w)) +#align category_theory.morphism_property.stable_under_cobase_change.respects_iso CategoryTheory.MorphismProperty.StableUnderCobaseChange.respectsIso + +theorem StableUnderCobaseChange.inl {P : MorphismProperty C} (hP : StableUnderCobaseChange P) + {A B A' : C} (f : A ⟶ A') (g : A ⟶ B) [HasPushout f g] (H : P g) : + P (pushout.inl : A' ⟶ pushout f g) := + hP (IsPushout.of_hasPushout f g) H +#align category_theory.morphism_property.stable_under_cobase_change.inl CategoryTheory.MorphismProperty.StableUnderCobaseChange.inl + +theorem StableUnderCobaseChange.inr {P : MorphismProperty C} (hP : StableUnderCobaseChange P) + {A B A' : C} (f : A ⟶ A') (g : A ⟶ B) [HasPushout f g] (H : P f) : + P (pushout.inr : B ⟶ pushout f g) := + hP (IsPushout.of_hasPushout f g).flip H +#align category_theory.morphism_property.stable_under_cobase_change.inr CategoryTheory.MorphismProperty.StableUnderCobaseChange.inr + +theorem StableUnderCobaseChange.op {P : MorphismProperty C} (hP : StableUnderCobaseChange P) : + StableUnderBaseChange P.op := fun _ _ _ _ _ _ _ _ sq hg => hP sq.unop hg +#align category_theory.morphism_property.stable_under_cobase_change.op CategoryTheory.MorphismProperty.StableUnderCobaseChange.op + +theorem StableUnderCobaseChange.unop {P : MorphismProperty Cᵒᵖ} (hP : StableUnderCobaseChange P) : + StableUnderBaseChange P.unop := fun _ _ _ _ _ _ _ _ sq hg => hP sq.op hg +#align category_theory.morphism_property.stable_under_cobase_change.unop CategoryTheory.MorphismProperty.StableUnderCobaseChange.unop + +theorem StableUnderBaseChange.op {P : MorphismProperty C} (hP : StableUnderBaseChange P) : + StableUnderCobaseChange P.op := fun _ _ _ _ _ _ _ _ sq hf => hP sq.unop hf +#align category_theory.morphism_property.stable_under_base_change.op CategoryTheory.MorphismProperty.StableUnderBaseChange.op + +theorem StableUnderBaseChange.unop {P : MorphismProperty Cᵒᵖ} (hP : StableUnderBaseChange P) : + StableUnderCobaseChange P.unop := fun _ _ _ _ _ _ _ _ sq hf => hP sq.op hf +#align category_theory.morphism_property.stable_under_base_change.unop CategoryTheory.MorphismProperty.StableUnderBaseChange.unop + +section + +variable (W : MorphismProperty C) + +/-- The property that a morphism property `W` is stable under limits +indexed by a category `J`. -/ +def IsStableUnderLimitsOfShape (J : Type*) [Category J] : Prop := + ∀ (X₁ X₂ : J ⥤ C) (c₁ : Cone X₁) (c₂ : Cone X₂) + (_ : IsLimit c₁) (h₂ : IsLimit c₂) (f : X₁ ⟶ X₂) (_ : W.functorCategory J f), + W (h₂.lift (Cone.mk _ (c₁.π ≫ f))) + +variable {W} + +lemma IsStableUnderLimitsOfShape.lim_map {J : Type*} [Category J] + (hW : W.IsStableUnderLimitsOfShape J) {X Y : J ⥤ C} + (f : X ⟶ Y) [HasLimitsOfShape J C] (hf : W.functorCategory _ f) : + W (lim.map f) := + hW X Y _ _ (limit.isLimit X) (limit.isLimit Y) f hf + +variable (W) + +/-- The property that a morphism property `W` is stable under products indexed by a type `J`. -/ +abbrev IsStableUnderProductsOfShape (J : Type*) := W.IsStableUnderLimitsOfShape (Discrete J) + +lemma IsStableUnderProductsOfShape.mk (J : Type*) + (hW₀ : W.RespectsIso) [HasProductsOfShape J C] + (hW : ∀ (X₁ X₂ : J → C) (f : ∀ j, X₁ j ⟶ X₂ j) (_ : ∀ (j : J), W (f j)), + W (Pi.map f)) : W.IsStableUnderProductsOfShape J := by + intro X₁ X₂ c₁ c₂ hc₁ hc₂ f hf + let φ := fun j => f.app (Discrete.mk j) + have hf' := hW _ _ φ (fun j => hf (Discrete.mk j)) + refine' (hW₀.arrow_mk_iso_iff _).2 hf' + refine' Arrow.isoMk + (IsLimit.conePointUniqueUpToIso hc₁ (limit.isLimit X₁) ≪≫ (Pi.isoLimit _).symm) + (IsLimit.conePointUniqueUpToIso hc₂ (limit.isLimit X₂) ≪≫ (Pi.isoLimit _).symm) _ + apply limit.hom_ext + rintro ⟨j⟩ + simp + +/-- The condition that a property of morphisms is stable by finite products. -/ +class IsStableUnderFiniteProducts : Prop := + isStableUnderProductsOfShape (J : Type) [Finite J] : W.IsStableUnderProductsOfShape J + +lemma isStableUnderProductsOfShape_of_isStableUnderFiniteProducts + (J : Type) [Finite J] [W.IsStableUnderFiniteProducts] : + W.IsStableUnderProductsOfShape J := + IsStableUnderFiniteProducts.isStableUnderProductsOfShape J + +end + +section Diagonal + +variable [HasPullbacks C] {P : MorphismProperty C} + +/-- For `P : MorphismProperty C`, `P.diagonal` is a morphism property that holds for `f : X ⟶ Y` +whenever `P` holds for `X ⟶ Y xₓ Y`. -/ +def diagonal (P : MorphismProperty C) : MorphismProperty C := fun _ _ f => P (pullback.diagonal f) +#align category_theory.morphism_property.diagonal CategoryTheory.MorphismProperty.diagonal + +theorem diagonal_iff {X Y : C} {f : X ⟶ Y} : P.diagonal f ↔ P (pullback.diagonal f) := + Iff.rfl +#align category_theory.morphism_property.diagonal_iff CategoryTheory.MorphismProperty.diagonal_iff + +theorem RespectsIso.diagonal (hP : P.RespectsIso) : P.diagonal.RespectsIso := by + constructor + · introv H + rwa [diagonal_iff, pullback.diagonal_comp, hP.cancel_left_isIso, hP.cancel_left_isIso, + ← hP.cancel_right_isIso _ + (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) (by simp) (by simp)), + ← pullback.condition, hP.cancel_left_isIso] + · introv H + delta diagonal + rwa [pullback.diagonal_comp, hP.cancel_right_isIso] +#align category_theory.morphism_property.respects_iso.diagonal CategoryTheory.MorphismProperty.RespectsIso.diagonal + +theorem StableUnderComposition.diagonal (hP : StableUnderComposition P) (hP' : RespectsIso P) + (hP'' : StableUnderBaseChange P) : P.diagonal.StableUnderComposition := by + introv X h₁ h₂ + rw [diagonal_iff, pullback.diagonal_comp] + exact hP _ _ h₁ (by simpa [hP'.cancel_left_isIso] using hP''.snd _ _ h₂) +#align category_theory.morphism_property.stable_under_composition.diagonal CategoryTheory.MorphismProperty.StableUnderComposition.diagonal + +theorem StableUnderBaseChange.diagonal (hP : StableUnderBaseChange P) (hP' : RespectsIso P) : + P.diagonal.StableUnderBaseChange := + StableUnderBaseChange.mk hP'.diagonal + (by + introv h + rw [diagonal_iff, diagonal_pullback_fst, hP'.cancel_left_isIso, hP'.cancel_right_isIso] + exact hP.baseChange_map f _ (by simpa)) +#align category_theory.morphism_property.stable_under_base_change.diagonal CategoryTheory.MorphismProperty.StableUnderBaseChange.diagonal + +end Diagonal + +section Universally + +/-- `P.universally` holds for a morphism `f : X ⟶ Y` iff `P` holds for all `X ×[Y] Y' ⟶ Y'`. -/ +def universally (P : MorphismProperty C) : MorphismProperty C := fun X Y f => + ∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y') (_ : IsPullback f' i₁ i₂ f), P f' +#align category_theory.morphism_property.universally CategoryTheory.MorphismProperty.universally + +theorem universally_respectsIso (P : MorphismProperty C) : P.universally.RespectsIso := by + constructor + · intro X Y Z e f hf X' Z' i₁ i₂ f' H + have : IsPullback (𝟙 _) (i₁ ≫ e.hom) i₁ e.inv := + IsPullback.of_horiz_isIso + ⟨by rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]⟩ + exact hf _ _ _ + (by simpa only [Iso.inv_hom_id_assoc, Category.id_comp] using this.paste_horiz H) + · intro X Y Z e f hf X' Z' i₁ i₂ f' H + have : IsPullback (𝟙 _) i₂ (i₂ ≫ e.inv) e.inv := + IsPullback.of_horiz_isIso ⟨Category.id_comp _⟩ + exact hf _ _ _ (by simpa only [Category.assoc, Iso.hom_inv_id, + Category.comp_id, Category.comp_id] using H.paste_horiz this) +#align category_theory.morphism_property.universally_respects_iso CategoryTheory.MorphismProperty.universally_respectsIso + +theorem universally_stableUnderBaseChange (P : MorphismProperty C) : + P.universally.StableUnderBaseChange := fun _ _ _ _ _ _ _ _ H h₁ _ _ _ _ _ H' => + h₁ _ _ _ (H'.paste_vert H.flip) +#align category_theory.morphism_property.universally_stable_under_base_change CategoryTheory.MorphismProperty.universally_stableUnderBaseChange + +theorem StableUnderComposition.universally [HasPullbacks C] {P : MorphismProperty C} + (hP : P.StableUnderComposition) : P.universally.StableUnderComposition := by + intro X Y Z f g hf hg X' Z' i₁ i₂ f' H + have := pullback.lift_fst _ _ (H.w.trans (Category.assoc _ _ _).symm) + rw [← this] at H ⊢ + apply hP _ _ _ (hg _ _ _ <| IsPullback.of_hasPullback _ _) + exact hf _ _ _ (H.of_right (pullback.lift_snd _ _ _) (IsPullback.of_hasPullback i₂ g)) +#align category_theory.morphism_property.stable_under_composition.universally CategoryTheory.MorphismProperty.StableUnderComposition.universally + +theorem universally_le (P : MorphismProperty C) : P.universally ≤ P := by + intro X Y f hf + exact hf (𝟙 _) (𝟙 _) _ (IsPullback.of_vert_isIso ⟨by rw [Category.comp_id, Category.id_comp]⟩) +#align category_theory.morphism_property.universally_le CategoryTheory.MorphismProperty.universally_le + +theorem StableUnderBaseChange.universally_eq {P : MorphismProperty C} + (hP : P.StableUnderBaseChange) : P.universally = P := + P.universally_le.antisymm fun _ _ _ hf _ _ _ _ _ H => hP H.flip hf +#align category_theory.morphism_property.stable_under_base_change.universally_eq CategoryTheory.MorphismProperty.StableUnderBaseChange.universally_eq + +theorem universally_mono : Monotone (universally : MorphismProperty C → MorphismProperty C) := + fun _ _ h _ _ _ h₁ _ _ _ _ _ H => h _ _ _ (h₁ _ _ _ H) +#align category_theory.morphism_property.universally_mono CategoryTheory.MorphismProperty.universally_mono + +end Universally + +end MorphismProperty + +end CategoryTheory From 941de72f7ae9e779715dd439c680df25b3d4dd1c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 24 Apr 2024 10:29:48 +0200 Subject: [PATCH 02/15] fixing files --- Mathlib.lean | 6 +++++- Mathlib/Algebra/Homology/ShortComplex/Exact.lean | 1 - Mathlib/AlgebraicGeometry/Morphisms/Basic.lean | 2 +- Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean | 4 +++- Mathlib/CategoryTheory/Localization/Construction.lean | 3 ++- Mathlib/CategoryTheory/Localization/FiniteProducts.lean | 1 + Mathlib/CategoryTheory/Localization/Pi.lean | 1 + Mathlib/CategoryTheory/Localization/Prod.lean | 2 ++ Mathlib/CategoryTheory/MorphismProperty/Basic.lean | 7 +++---- Mathlib/CategoryTheory/MorphismProperty/Concrete.lean | 1 + Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean | 1 + Mathlib/CategoryTheory/MorphismProperty/Limits.lean | 2 ++ 12 files changed, 22 insertions(+), 9 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index d2a0de8dfda3e..ca21ef2f4756c 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1428,7 +1428,11 @@ import Mathlib.CategoryTheory.Monoidal.Transport import Mathlib.CategoryTheory.Monoidal.Types.Basic import Mathlib.CategoryTheory.Monoidal.Types.Coyoneda import Mathlib.CategoryTheory.Monoidal.Types.Symmetric -import Mathlib.CategoryTheory.MorphismProperty +import Mathlib.CategoryTheory.MorphismProperty.Basic +import Mathlib.CategoryTheory.MorphismProperty.Composition +import Mathlib.CategoryTheory.MorphismProperty.Concrete +import Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy +import Mathlib.CategoryTheory.MorphismProperty.Limits import Mathlib.CategoryTheory.NatIso import Mathlib.CategoryTheory.NatTrans import Mathlib.CategoryTheory.Noetherian diff --git a/Mathlib/Algebra/Homology/ShortComplex/Exact.lean b/Mathlib/Algebra/Homology/ShortComplex/Exact.lean index 2d64cd5fe997f..13c4e615c78e0 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/Exact.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/Exact.lean @@ -7,7 +7,6 @@ import Mathlib.Algebra.Homology.ShortComplex.PreservesHomology import Mathlib.Algebra.Homology.ShortComplex.Abelian import Mathlib.Algebra.Homology.ShortComplex.QuasiIso import Mathlib.CategoryTheory.Abelian.Exact -import Mathlib.CategoryTheory.MorphismProperty import Mathlib.CategoryTheory.Preadditive.Injective /-! diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean b/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean index 58f0180513868..65495ac51f001 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean @@ -5,7 +5,7 @@ Authors: Andrew Yang -/ import Mathlib.AlgebraicGeometry.AffineScheme import Mathlib.AlgebraicGeometry.Pullbacks -import Mathlib.CategoryTheory.MorphismProperty +import Mathlib.CategoryTheory.MorphismProperty.Limits import Mathlib.Data.List.TFAE #align_import algebraic_geometry.morphisms.basic from "leanprover-community/mathlib"@"434e2fd21c1900747afc6d13d8be7f4eedba7218" diff --git a/Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean b/Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean index 086d0c8dca81b..6e1f75de2d8fc 100644 --- a/Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean +++ b/Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean @@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ import Mathlib.CategoryTheory.Conj -import Mathlib.CategoryTheory.MorphismProperty +import Mathlib.CategoryTheory.Adjunction.Basic +import Mathlib.CategoryTheory.MorphismProperty.Basic +import Mathlib.CategoryTheory.Yoneda #align_import category_theory.adjunction.fully_faithful from "leanprover-community/mathlib"@"9e7c80f638149bfb3504ba8ff48dfdbfc949fb1a" diff --git a/Mathlib/CategoryTheory/Localization/Construction.lean b/Mathlib/CategoryTheory/Localization/Construction.lean index a9da1153d0b32..36a5ebbd006ac 100644 --- a/Mathlib/CategoryTheory/Localization/Construction.lean +++ b/Mathlib/CategoryTheory/Localization/Construction.lean @@ -3,7 +3,8 @@ Copyright (c) 2022 Joël Riou. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joël Riou -/ -import Mathlib.CategoryTheory.MorphismProperty +import Mathlib.CategoryTheory.MorphismProperty.Composition +import Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy import Mathlib.CategoryTheory.Category.Quiv #align_import category_theory.localization.construction from "leanprover-community/mathlib"@"1a5e56f2166e4e9d0964c71f4273b1d39227678d" diff --git a/Mathlib/CategoryTheory/Localization/FiniteProducts.lean b/Mathlib/CategoryTheory/Localization/FiniteProducts.lean index 0ed40a832d194..045f79314e84d 100644 --- a/Mathlib/CategoryTheory/Localization/FiniteProducts.lean +++ b/Mathlib/CategoryTheory/Localization/FiniteProducts.lean @@ -8,6 +8,7 @@ import Mathlib.CategoryTheory.Limits.Preserves.Finite import Mathlib.CategoryTheory.Localization.Adjunction import Mathlib.CategoryTheory.Localization.HasLocalization import Mathlib.CategoryTheory.Localization.Pi +import Mathlib.CategoryTheory.MorphismProperty.Limits /-! The localized category has finite products diff --git a/Mathlib/CategoryTheory/Localization/Pi.lean b/Mathlib/CategoryTheory/Localization/Pi.lean index 9d907e03fc2d3..72cc12ff2667e 100644 --- a/Mathlib/CategoryTheory/Localization/Pi.lean +++ b/Mathlib/CategoryTheory/Localization/Pi.lean @@ -5,6 +5,7 @@ Authors: Joël Riou -/ import Mathlib.CategoryTheory.Localization.Prod import Mathlib.CategoryTheory.Localization.Equivalence +import Mathlib.Data.Fintype.Option /-! # Localization of product categories diff --git a/Mathlib/CategoryTheory/Localization/Prod.lean b/Mathlib/CategoryTheory/Localization/Prod.lean index 62762e7f46073..0add5c3d8de6c 100644 --- a/Mathlib/CategoryTheory/Localization/Prod.lean +++ b/Mathlib/CategoryTheory/Localization/Prod.lean @@ -3,7 +3,9 @@ Copyright (c) 2023 Joël Riou. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joël Riou -/ +import Mathlib.CategoryTheory.Functor.Currying import Mathlib.CategoryTheory.Localization.Predicate +import Mathlib.CategoryTheory.MorphismProperty.Composition /-! # Localization of product categories diff --git a/Mathlib/CategoryTheory/MorphismProperty/Basic.lean b/Mathlib/CategoryTheory/MorphismProperty/Basic.lean index ea9127db921bc..f6b75a979de9e 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Basic.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Basic.lean @@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Andrew Yang -/ import Mathlib.CategoryTheory.Comma.Arrow -import Mathlib.CategoryTheory.ConcreteCategory.Basic -import Mathlib.CategoryTheory.Limits.Shapes.CommSq -import Mathlib.CategoryTheory.Limits.Shapes.Diagonal +import Mathlib.CategoryTheory.Pi.Basic +import Mathlib.Order.CompleteLattice #align_import category_theory.morphism_property from "leanprover-community/mathlib"@"7f963633766aaa3ebc8253100a5229dd463040c7" @@ -24,7 +23,7 @@ The following meta-property is defined universe w v v' u u' -open CategoryTheory CategoryTheory.Limits Opposite +open CategoryTheory Opposite noncomputable section diff --git a/Mathlib/CategoryTheory/MorphismProperty/Concrete.lean b/Mathlib/CategoryTheory/MorphismProperty/Concrete.lean index 947bed31cbaae..aeedcafc9c3a1 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Concrete.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Concrete.lean @@ -3,6 +3,7 @@ Copyright (c) 2022 Andrew Yang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Andrew Yang -/ +import Mathlib.CategoryTheory.ConcreteCategory.Basic import Mathlib.CategoryTheory.MorphismProperty.Composition /-! diff --git a/Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean b/Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean index fde6405d93e47..145dc072ca628 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean @@ -3,6 +3,7 @@ Copyright (c) 2022 Joël Riou. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joël Riou -/ +import Mathlib.CategoryTheory.Functor.ReflectsIso import Mathlib.CategoryTheory.MorphismProperty.Basic /-! diff --git a/Mathlib/CategoryTheory/MorphismProperty/Limits.lean b/Mathlib/CategoryTheory/MorphismProperty/Limits.lean index 1971ab46fb994..e204ae2ea1f69 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Limits.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Limits.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Andrew Yang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Andrew Yang, Joël Riou -/ +import Mathlib.CategoryTheory.Limits.Shapes.CommSq +import Mathlib.CategoryTheory.Limits.Shapes.Diagonal import Mathlib.CategoryTheory.MorphismProperty.Composition /-! From 34e100c154d0dec32f7472f15eb73b7ed35a8c05 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 24 Apr 2024 10:42:37 +0200 Subject: [PATCH 03/15] fixing the build --- Mathlib/Algebra/Homology/HomotopyCategory.lean | 1 + Mathlib/Algebra/Homology/HomotopyCofiber.lean | 1 + Mathlib/Algebra/Homology/Localization.lean | 4 ++-- 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Homology/HomotopyCategory.lean b/Mathlib/Algebra/Homology/HomotopyCategory.lean index fc632dfa0bb8d..9e0a6caff6c71 100644 --- a/Mathlib/Algebra/Homology/HomotopyCategory.lean +++ b/Mathlib/Algebra/Homology/HomotopyCategory.lean @@ -5,6 +5,7 @@ Authors: Scott Morrison -/ import Mathlib.Algebra.Homology.Homotopy import Mathlib.Algebra.Homology.Linear +import Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy import Mathlib.CategoryTheory.Quotient.Linear import Mathlib.CategoryTheory.Quotient.Preadditive diff --git a/Mathlib/Algebra/Homology/HomotopyCofiber.lean b/Mathlib/Algebra/Homology/HomotopyCofiber.lean index bb3c1d2bf08ad..97e42a3d54a21 100644 --- a/Mathlib/Algebra/Homology/HomotopyCofiber.lean +++ b/Mathlib/Algebra/Homology/HomotopyCofiber.lean @@ -5,6 +5,7 @@ Authors: Joël Riou -/ import Mathlib.Algebra.Homology.HomologicalComplexBiprod import Mathlib.Algebra.Homology.Homotopy +import Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy /-! The homotopy cofiber of a morphism of homological complexes diff --git a/Mathlib/Algebra/Homology/Localization.lean b/Mathlib/Algebra/Homology/Localization.lean index 44a78f2f058fd..8a38d8959446c 100644 --- a/Mathlib/Algebra/Homology/Localization.lean +++ b/Mathlib/Algebra/Homology/Localization.lean @@ -5,10 +5,10 @@ Authors: Joël Riou -/ import Mathlib.Algebra.Homology.HomotopyCofiber -import Mathlib.Algebra.Homology.QuasiIso import Mathlib.Algebra.Homology.HomotopyCategory -import Mathlib.CategoryTheory.Localization.HasLocalization +import Mathlib.Algebra.Homology.QuasiIso import Mathlib.CategoryTheory.Localization.Composition +import Mathlib.CategoryTheory.Localization.HasLocalization /-! The category of homological complexes up to quasi-isomorphisms From 16695f4f9d0c5f2f691f90550bdc58fd894baabd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 24 Apr 2024 21:12:04 +0200 Subject: [PATCH 04/15] the two out of three property --- .../MorphismProperty/Basic.lean | 4 + .../MorphismProperty/Composition.lean | 171 +++++++++++------- .../MorphismProperty/Concrete.lean | 61 ++++--- .../MorphismProperty/Limits.lean | 30 +-- 4 files changed, 161 insertions(+), 105 deletions(-) diff --git a/Mathlib/CategoryTheory/MorphismProperty/Basic.lean b/Mathlib/CategoryTheory/MorphismProperty/Basic.lean index f6b75a979de9e..21bd60143e71a 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Basic.lean +++ b/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) diff --git a/Mathlib/CategoryTheory/MorphismProperty/Composition.lean b/Mathlib/CategoryTheory/MorphismProperty/Composition.lean index d761dc8749721..109a2417ec2c6 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Composition.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Composition.lean @@ -8,13 +8,12 @@ import Mathlib.CategoryTheory.MorphismProperty.Basic /-! # Compatibilities of properties of morphisms with respect to composition -Given `P : MorphismProperty C`, we define the predicate `P.StableUnderComposition` +Given `P : MorphismProperty C`, we define the predicate `P.IsStableUnderComposition` which means that `P f → P g → P (f ≫ g)`. We also introduce the type classes `W.ContainsIdentities` and `W.IsMultiplicative`. ## TODO * define the type class of morphism properties that satisfy the 2-out-of-3 property -(which may require transforming `StableUnderComposition` into a type class) -/ @@ -30,10 +29,10 @@ variable {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D] /-- Typeclass expressing that a morphism property contain identities. -/ class ContainsIdentities (W : MorphismProperty C) : Prop := /-- for all `X : C`, the identity of `X` satisfies the morphism property -/ - id_mem' : ∀ (X : C), W (𝟙 X) + id_mem : ∀ (X : C), W (𝟙 X) lemma id_mem (W : MorphismProperty C) [W.ContainsIdentities] (X : C) : - W (𝟙 X) := ContainsIdentities.id_mem' X + W (𝟙 X) := ContainsIdentities.id_mem X namespace ContainsIdentities @@ -49,6 +48,10 @@ lemma of_op (W : MorphismProperty C) [W.op.ContainsIdentities] : lemma of_unop (W : MorphismProperty Cᵒᵖ) [W.unop.ContainsIdentities] : W.ContainsIdentities := (inferInstance : W.unop.op.ContainsIdentities) +instance inverseImage {P : MorphismProperty D} [P.ContainsIdentities] (F : C ⥤ D) : + (P.inverseImage F).ContainsIdentities where + id_mem X := by simpa only [← F.map_id] using P.id_mem (F.obj X) + end ContainsIdentities instance Prod.containsIdentities {C₁ C₂ : Type*} [Category C₁] [Category C₂] @@ -61,19 +64,25 @@ instance Pi.containsIdentities {J : Type w} {C : J → Type u} (pi W).ContainsIdentities := ⟨fun _ _ => MorphismProperty.id_mem _ _⟩ -/-- A morphism property is `StableUnderComposition` if the composition of two such morphisms -still falls in the class. -/ -def StableUnderComposition (P : MorphismProperty C) : Prop := - ∀ ⦃X Y Z⦄ (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → P (f ≫ g) -#align category_theory.morphism_property.stable_under_composition CategoryTheory.MorphismProperty.StableUnderComposition +/-- A morphism property satisfies `IsStableUnderComposition` if the composition of +two such morphisms still falls in the class. -/ +class IsStableUnderComposition (P : MorphismProperty C) : Prop := + comp_mem {X Y Z} (f : X ⟶ Y) (g : Y ⟶ Z) : P f → P g → P (f ≫ g) +#align category_theory.morphism_property.stable_under_composition CategoryTheory.MorphismProperty.IsStableUnderComposition + +lemma comp_mem (W : MorphismProperty C) [W.IsStableUnderComposition] + {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : W f) (hg : W g) : W (f ≫ g) := + IsStableUnderComposition.comp_mem f g hf hg -theorem StableUnderComposition.op {P : MorphismProperty C} (h : StableUnderComposition P) : - StableUnderComposition P.op := fun _ _ _ f g hf hg => h g.unop f.unop hg hf -#align category_theory.morphism_property.stable_under_composition.op CategoryTheory.MorphismProperty.StableUnderComposition.op +instance IsStableUnderComposition.op {P : MorphismProperty C} [P.IsStableUnderComposition] : + P.op.IsStableUnderComposition where + comp_mem f g hf hg := P.comp_mem g.unop f.unop hg hf +#align category_theory.morphism_property.stable_under_composition.op CategoryTheory.MorphismProperty.IsStableUnderComposition.op -theorem StableUnderComposition.unop {P : MorphismProperty Cᵒᵖ} (h : StableUnderComposition P) : - StableUnderComposition P.unop := fun _ _ _ f g hf hg => h g.op f.op hg hf -#align category_theory.morphism_property.stable_under_composition.unop CategoryTheory.MorphismProperty.StableUnderComposition.unop +theorem IsStableUnderComposition.unop {P : MorphismProperty Cᵒᵖ} [P.IsStableUnderComposition] : + P.unop.IsStableUnderComposition where + comp_mem f g hf hg := P.comp_mem g.op f.op hg hf +#align category_theory.morphism_property.stable_under_composition.unop CategoryTheory.MorphismProperty.IsStableUnderComposition.unop /-- A morphism property is `StableUnderInverse` if the inverse of a morphism satisfying the property still falls in the class. -/ @@ -89,39 +98,15 @@ theorem StableUnderInverse.unop {P : MorphismProperty Cᵒᵖ} (h : StableUnderI StableUnderInverse P.unop := fun _ _ e he => h e.op he #align category_theory.morphism_property.stable_under_inverse.unop CategoryTheory.MorphismProperty.StableUnderInverse.unop -theorem StableUnderComposition.respectsIso {P : MorphismProperty C} (hP : StableUnderComposition P) - (hP' : ∀ {X Y} (e : X ≅ Y), P e.hom) : RespectsIso P := - ⟨fun e _ hf => hP _ _ (hP' e) hf, fun e _ hf => hP _ _ hf (hP' e)⟩ -#align category_theory.morphism_property.stable_under_composition.respects_iso CategoryTheory.MorphismProperty.StableUnderComposition.respectsIso - -theorem StableUnderComposition.isomorphisms : StableUnderComposition (isomorphisms C) := - fun X Y Z f g hf hg => by - rw [isomorphisms.iff] at hf hg ⊢ - haveI := hf - haveI := hg - infer_instance -#align category_theory.morphism_property.stable_under_composition.isomorphisms CategoryTheory.MorphismProperty.StableUnderComposition.isomorphisms - -theorem StableUnderComposition.monomorphisms : StableUnderComposition (monomorphisms C) := - fun X Y Z f g hf hg => by - rw [monomorphisms.iff] at hf hg ⊢ - haveI := hf - haveI := hg - apply mono_comp -#align category_theory.morphism_property.stable_under_composition.monomorphisms CategoryTheory.MorphismProperty.StableUnderComposition.monomorphisms - -theorem StableUnderComposition.epimorphisms : StableUnderComposition (epimorphisms C) := - fun X Y Z f g hf hg => by - rw [epimorphisms.iff] at hf hg ⊢ - haveI := hf - haveI := hg - apply epi_comp -#align category_theory.morphism_property.stable_under_composition.epimorphisms CategoryTheory.MorphismProperty.StableUnderComposition.epimorphisms - -theorem StableUnderComposition.inverseImage {P : MorphismProperty D} (h : StableUnderComposition P) - (F : C ⥤ D) : StableUnderComposition (P.inverseImage F) := fun X Y Z f g hf hg => by - simpa only [← F.map_comp] using h (F.map f) (F.map g) hf hg -#align category_theory.morphism_property.stable_under_composition.inverse_image CategoryTheory.MorphismProperty.StableUnderComposition.inverseImage +theorem respectsIso_of_isStableUnderComposition {P : MorphismProperty C} [P.IsStableUnderComposition] + (hP : isomorphisms C ⊆ P) : RespectsIso P := + ⟨fun _ _ hf => P.comp_mem _ _ (hP _ (isomorphisms.infer_property _)) hf, + fun _ _ hf => P.comp_mem _ _ hf (hP _ (isomorphisms.infer_property _))⟩ +#align category_theory.morphism_property.stable_under_composition.respects_iso CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition + +instance IsStableUnderComposition.inverseImage {P : MorphismProperty D} [P.IsStableUnderComposition] + (F : C ⥤ D) : (P.inverseImage F).IsStableUnderComposition where + comp_mem f g hf hg := by simpa only [← F.map_comp] using P.comp_mem _ _ hf hg /-- Given `app : Π X, F₁.obj X ⟶ F₂.obj X` where `F₁` and `F₂` are two functors, this is the `morphism_property C` satisfied by the morphisms in `C` with respect @@ -133,13 +118,14 @@ def naturalityProperty {F₁ F₂ : C ⥤ D} (app : ∀ X, F₁.obj X ⟶ F₂.o namespace naturalityProperty -theorem stableUnderComposition {F₁ F₂ : C ⥤ D} (app : ∀ X, F₁.obj X ⟶ F₂.obj X) : - (naturalityProperty app).StableUnderComposition := fun X Y Z f g hf hg => by - simp only [naturalityProperty] at hf hg ⊢ - simp only [Functor.map_comp, Category.assoc, hg] - slice_lhs 1 2 => rw [hf] - rw [Category.assoc] -#align category_theory.morphism_property.naturality_property.is_stable_under_composition CategoryTheory.MorphismProperty.naturalityProperty.stableUnderComposition +instance isStableUnderComposition {F₁ F₂ : C ⥤ D} (app : ∀ X, F₁.obj X ⟶ F₂.obj X) : + (naturalityProperty app).IsStableUnderComposition where + comp_mem f g hf hg := by + simp only [naturalityProperty] at hf hg ⊢ + simp only [Functor.map_comp, Category.assoc, hg] + slice_lhs 1 2 => rw [hf] + rw [Category.assoc] +#align category_theory.morphism_property.naturality_property.is_stable_under_composition CategoryTheory.MorphismProperty.naturalityProperty.isStableUnderComposition theorem stableUnderInverse {F₁ F₂ : C ⥤ D} (app : ∀ X, F₁.obj X ⟶ F₂.obj X) : (naturalityProperty app).StableUnderInverse := fun X Y e he => by @@ -154,21 +140,17 @@ end naturalityProperty /-- A morphism property is multiplicative if it contains identities and is stable by composition. -/ -class IsMultiplicative (W : MorphismProperty C) extends W.ContainsIdentities : Prop := - stableUnderComposition : W.StableUnderComposition - -lemma comp_mem (W : MorphismProperty C) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : W f) (hg : W g) - [IsMultiplicative W] : W (f ≫ g) := - IsMultiplicative.stableUnderComposition f g hf hg +class IsMultiplicative (W : MorphismProperty C) + extends W.ContainsIdentities, W.IsStableUnderComposition : Prop := namespace IsMultiplicative instance op (W : MorphismProperty C) [IsMultiplicative W] : IsMultiplicative W.op where - stableUnderComposition := fun _ _ _ f g hf hg => W.comp_mem g.unop f.unop hg hf + comp_mem f g hf hg := W.comp_mem g.unop f.unop hg hf instance unop (W : MorphismProperty Cᵒᵖ) [IsMultiplicative W] : IsMultiplicative W.unop where - id_mem' _ := W.id_mem _ - stableUnderComposition := fun _ _ _ f g hf hg => W.comp_mem g.op f.op hg hf + id_mem _ := W.id_mem _ + comp_mem f g hf hg := W.comp_mem g.op f.op hg hf lemma of_op (W : MorphismProperty C) [IsMultiplicative W.op] : IsMultiplicative W := (inferInstance : IsMultiplicative W.op.unop) @@ -176,8 +158,69 @@ lemma of_op (W : MorphismProperty C) [IsMultiplicative W.op] : IsMultiplicative lemma of_unop (W : MorphismProperty Cᵒᵖ) [IsMultiplicative W.unop] : IsMultiplicative W := (inferInstance : IsMultiplicative W.unop.op) +instance : (isomorphisms C).IsMultiplicative where + id_mem _ := isomorphisms.infer_property _ + comp_mem f g hf hg := by + rw [isomorphisms.iff] at hf hg ⊢ + infer_instance + +instance : (monomorphisms C).IsMultiplicative where + id_mem _ := monomorphisms.infer_property _ + comp_mem f g hf hg := by + rw [monomorphisms.iff] at hf hg ⊢ + apply mono_comp + +instance : (epimorphisms C).IsMultiplicative where + id_mem _ := epimorphisms.infer_property _ + comp_mem f g hf hg := by + rw [epimorphisms.iff] at hf hg ⊢ + apply epi_comp + +instance {P : MorphismProperty D} [P.IsMultiplicative] (F : C ⥤ D) : + (P.inverseImage F).IsMultiplicative where + end IsMultiplicative +/-- A class of morphisms `W` has the two-out-of-three property if whenever two out +of three maps in `f`, `g`, `f ≫ g` are in `W`, then the third map is also in `W`. -/ +class HasTwoOutOfThreeProperty (W : MorphismProperty C) + extends W.IsStableUnderComposition : Prop where + of_postcomp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : W g → W (f ≫ g) → W f + of_precomp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : W f → W (f ≫ g) → W g + +section + +variable (W : MorphismProperty C) [W.HasTwoOutOfThreeProperty] + +lemma of_postcomp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hg : W g) (hfg : W (f ≫ g)) : + W f := + HasTwoOutOfThreeProperty.of_postcomp f g hg hfg + +lemma of_precomp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : W f) (hfg : W (f ≫ g)) : + W g := + HasTwoOutOfThreeProperty.of_precomp f g hf hfg + +lemma postcomp_iff {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hg : W g) : + W (f ≫ g) ↔ W f := + ⟨W.of_postcomp f g hg, fun hf => W.comp_mem _ _ hf hg⟩ + +lemma precomp_iff {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : W f) : + W (f ≫ g) ↔ W g := + ⟨W.of_precomp f g hf, fun hg => W.comp_mem _ _ hf hg⟩ + +end + +instance : (isomorphisms C).HasTwoOutOfThreeProperty where + of_postcomp f g := fun (hg : IsIso g) (hfg : IsIso (f ≫ g)) => + by simpa using (inferInstance : IsIso ((f ≫ g) ≫ inv g)) + of_precomp f g := fun (hf : IsIso f) (hfg : IsIso (f ≫ g)) => + by simpa using (inferInstance : IsIso (inv f ≫ (f ≫ g))) + +instance (F : C ⥤ D) (W : MorphismProperty D) [W.HasTwoOutOfThreeProperty] : + (W.inverseImage F).HasTwoOutOfThreeProperty where + of_postcomp f g hg hfg := W.of_postcomp (F.map f) (F.map g) hg (by simpa using hfg) + of_precomp f g hf hfg := W.of_precomp (F.map f) (F.map g) hf (by simpa using hfg) + end MorphismProperty end CategoryTheory diff --git a/Mathlib/CategoryTheory/MorphismProperty/Concrete.lean b/Mathlib/CategoryTheory/MorphismProperty/Concrete.lean index aeedcafc9c3a1..bce6f81066317 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Concrete.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Concrete.lean @@ -44,40 +44,49 @@ theorem bijective_eq_sup : rfl #align category_theory.morphism_property.bijective_eq_sup CategoryTheory.MorphismProperty.bijective_eq_sup -theorem injective_stableUnderComposition : (MorphismProperty.injective C).StableUnderComposition := - fun X Y Z f g hf hg => by - delta MorphismProperty.injective - rw [coe_comp] - exact hg.comp hf -#align category_theory.morphism_property.injective_stable_under_composition CategoryTheory.MorphismProperty.injective_stableUnderComposition - -theorem surjective_stableUnderComposition : - (MorphismProperty.surjective C).StableUnderComposition := fun X Y Z f g hf hg => by - delta MorphismProperty.surjective - rw [coe_comp] - exact hg.comp hf -#align category_theory.morphism_property.surjective_stable_under_composition CategoryTheory.MorphismProperty.surjective_stableUnderComposition - -theorem bijective_stableUnderComposition : (MorphismProperty.bijective C).StableUnderComposition := - fun X Y Z f g hf hg => by - delta MorphismProperty.bijective - rw [coe_comp] - exact hg.comp hf -#align category_theory.morphism_property.bijective_stable_under_composition CategoryTheory.MorphismProperty.bijective_stableUnderComposition +instance : (MorphismProperty.injective C).IsMultiplicative where + id_mem X := by + delta MorphismProperty.injective + convert injective_id + aesop + comp_mem f g hf hg := by + delta MorphismProperty.injective + rw [coe_comp] + exact hg.comp hf + +instance : (MorphismProperty.surjective C).IsMultiplicative where + id_mem X := by + delta MorphismProperty.surjective + convert surjective_id + aesop + comp_mem f g hf hg := by + delta MorphismProperty.surjective + rw [coe_comp] + exact hg.comp hf + +instance : (MorphismProperty.bijective C).IsMultiplicative where + id_mem X := by + delta MorphismProperty.bijective + convert bijective_id + aesop + comp_mem f g hf hg := by + delta MorphismProperty.bijective + rw [coe_comp] + exact hg.comp hf theorem injective_respectsIso : (MorphismProperty.injective C).RespectsIso := - (injective_stableUnderComposition C).respectsIso - (fun e => ((forget C).mapIso e).toEquiv.injective) + respectsIso_of_isStableUnderComposition + (fun _ _ f (_ : IsIso f) => ((forget C).mapIso (asIso f)).toEquiv.injective) #align category_theory.morphism_property.injective_respects_iso CategoryTheory.MorphismProperty.injective_respectsIso theorem surjective_respectsIso : (MorphismProperty.surjective C).RespectsIso := - (surjective_stableUnderComposition C).respectsIso - (fun e => ((forget C).mapIso e).toEquiv.surjective) + respectsIso_of_isStableUnderComposition + (fun _ _ f (_ : IsIso f) => ((forget C).mapIso (asIso f)).toEquiv.surjective) #align category_theory.morphism_property.surjective_respects_iso CategoryTheory.MorphismProperty.surjective_respectsIso theorem bijective_respectsIso : (MorphismProperty.bijective C).RespectsIso := - (bijective_stableUnderComposition C).respectsIso - (fun e => ((forget C).mapIso e).toEquiv.bijective) + respectsIso_of_isStableUnderComposition + (fun _ _ f (_ : IsIso f) => ((forget C).mapIso (asIso f)).toEquiv.bijective) #align category_theory.morphism_property.bijective_respects_iso CategoryTheory.MorphismProperty.bijective_respectsIso end MorphismProperty diff --git a/Mathlib/CategoryTheory/MorphismProperty/Limits.lean b/Mathlib/CategoryTheory/MorphismProperty/Limits.lean index e204ae2ea1f69..99b0e28be3c5d 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Limits.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Limits.lean @@ -93,7 +93,7 @@ theorem StableUnderBaseChange.baseChange_map [HasPullbacks C] {P : MorphismPrope #align category_theory.morphism_property.stable_under_base_change.base_change_map CategoryTheory.MorphismProperty.StableUnderBaseChange.baseChange_map theorem StableUnderBaseChange.pullback_map [HasPullbacks C] {P : MorphismProperty C} - (hP : StableUnderBaseChange P) (hP' : StableUnderComposition P) {S X X' Y Y' : C} {f : X ⟶ S} + (hP : StableUnderBaseChange P) [P.IsStableUnderComposition] {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₂ (𝟙 _) ((Category.comp_id _).trans e₁) @@ -107,7 +107,7 @@ theorem StableUnderBaseChange.pullback_map [HasPullbacks C] {P : MorphismPropert ((baseChange g').map (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f')).left := by ext <;> dsimp <;> simp rw [this] - apply hP' <;> rw [hP.respectsIso.cancel_left_isIso] + apply P.comp_mem <;> rw [hP.respectsIso.cancel_left_isIso] exacts [hP.baseChange_map _ (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g') h₂, hP.baseChange_map _ (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f') h₁] #align category_theory.morphism_property.stable_under_base_change.pullback_map CategoryTheory.MorphismProperty.StableUnderBaseChange.pullback_map @@ -228,11 +228,11 @@ theorem RespectsIso.diagonal (hP : P.RespectsIso) : P.diagonal.RespectsIso := by rwa [pullback.diagonal_comp, hP.cancel_right_isIso] #align category_theory.morphism_property.respects_iso.diagonal CategoryTheory.MorphismProperty.RespectsIso.diagonal -theorem StableUnderComposition.diagonal (hP : StableUnderComposition P) (hP' : RespectsIso P) - (hP'' : StableUnderBaseChange P) : P.diagonal.StableUnderComposition := by - introv X h₁ h₂ - rw [diagonal_iff, pullback.diagonal_comp] - exact hP _ _ h₁ (by simpa [hP'.cancel_left_isIso] using hP''.snd _ _ h₂) +theorem StableUnderComposition.diagonal [P.IsStableUnderComposition] (hP' : RespectsIso P) + (hP'' : StableUnderBaseChange P) : P.diagonal.IsStableUnderComposition where + comp_mem _ _ h₁ h₂ := by + rw [diagonal_iff, pullback.diagonal_comp] + exact P.comp_mem _ _ h₁ (by simpa [hP'.cancel_left_isIso] using hP''.snd _ _ h₂) #align category_theory.morphism_property.stable_under_composition.diagonal CategoryTheory.MorphismProperty.StableUnderComposition.diagonal theorem StableUnderBaseChange.diagonal (hP : StableUnderBaseChange P) (hP' : RespectsIso P) : @@ -273,14 +273,14 @@ theorem universally_stableUnderBaseChange (P : MorphismProperty C) : h₁ _ _ _ (H'.paste_vert H.flip) #align category_theory.morphism_property.universally_stable_under_base_change CategoryTheory.MorphismProperty.universally_stableUnderBaseChange -theorem StableUnderComposition.universally [HasPullbacks C] {P : MorphismProperty C} - (hP : P.StableUnderComposition) : P.universally.StableUnderComposition := by - intro X Y Z f g hf hg X' Z' i₁ i₂ f' H - have := pullback.lift_fst _ _ (H.w.trans (Category.assoc _ _ _).symm) - rw [← this] at H ⊢ - apply hP _ _ _ (hg _ _ _ <| IsPullback.of_hasPullback _ _) - exact hf _ _ _ (H.of_right (pullback.lift_snd _ _ _) (IsPullback.of_hasPullback i₂ g)) -#align category_theory.morphism_property.stable_under_composition.universally CategoryTheory.MorphismProperty.StableUnderComposition.universally +instance IsStableUnderComposition.universally [HasPullbacks C] (P : MorphismProperty C) + [hP : P.IsStableUnderComposition] : P.universally.IsStableUnderComposition where + comp_mem {X Y Z} f g hf hg X' Z' i₁ i₂ f' H := by + have := pullback.lift_fst _ _ (H.w.trans (Category.assoc _ _ _).symm) + rw [← this] at H ⊢ + apply P.comp_mem _ _ _ (hg _ _ _ <| IsPullback.of_hasPullback _ _) + exact hf _ _ _ (H.of_right (pullback.lift_snd _ _ _) (IsPullback.of_hasPullback i₂ g)) +#align category_theory.morphism_property.stable_under_composition.universally CategoryTheory.MorphismProperty.IsStableUnderComposition.universally theorem universally_le (P : MorphismProperty C) : P.universally ≤ P := by intro X Y f hf From f3ad8a1c997d6bcc79984934ae2c9359869b8d19 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 26 Apr 2024 19:09:28 +0200 Subject: [PATCH 05/15] fixing the build --- Mathlib/CategoryTheory/Adjunction/Reflective.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/CategoryTheory/Adjunction/Reflective.lean b/Mathlib/CategoryTheory/Adjunction/Reflective.lean index b22c920d61a1d..6bcf9f71d2b0d 100644 --- a/Mathlib/CategoryTheory/Adjunction/Reflective.lean +++ b/Mathlib/CategoryTheory/Adjunction/Reflective.lean @@ -5,6 +5,7 @@ Authors: Bhavik Mehta -/ import Mathlib.CategoryTheory.Adjunction.FullyFaithful import Mathlib.CategoryTheory.Conj +import Mathlib.CategoryTheory.Functor.ReflectsIso #align_import category_theory.adjunction.reflective from "leanprover-community/mathlib"@"239d882c4fb58361ee8b3b39fb2091320edef10a" From 37ae07027b139f1c5976dac9bcd507cbf4d88c08 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 26 Apr 2024 19:17:24 +0200 Subject: [PATCH 06/15] fixing the build --- Mathlib/CategoryTheory/Subobject/MonoOver.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/CategoryTheory/Subobject/MonoOver.lean b/Mathlib/CategoryTheory/Subobject/MonoOver.lean index 8f2b87f530867..56a316b2a6136 100644 --- a/Mathlib/CategoryTheory/Subobject/MonoOver.lean +++ b/Mathlib/CategoryTheory/Subobject/MonoOver.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Bhavik Mehta, Scott Morrison -/ import Mathlib.CategoryTheory.Limits.Over +import Mathlib.CategoryTheory.Limits.Shapes.Images import Mathlib.CategoryTheory.Adjunction.Reflective import Mathlib.CategoryTheory.Adjunction.Restrict From d3e7ce21b0bb0e9d46e3496b8c4547e5596e5100 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 26 Apr 2024 19:49:30 +0200 Subject: [PATCH 07/15] fixing the build --- Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean b/Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean index d583353518427..a2da37fb1f348 100644 --- a/Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean +++ b/Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean @@ -3,7 +3,6 @@ Copyright (c) 2019 Scott Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ -import Mathlib.CategoryTheory.Conj import Mathlib.CategoryTheory.Adjunction.Basic import Mathlib.CategoryTheory.MorphismProperty.Basic import Mathlib.CategoryTheory.Yoneda From 105eea817d05a4905422a518a2695ea9d15b63ed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 26 Apr 2024 22:56:02 +0200 Subject: [PATCH 08/15] fixed long line --- Mathlib/CategoryTheory/MorphismProperty/Composition.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/MorphismProperty/Composition.lean b/Mathlib/CategoryTheory/MorphismProperty/Composition.lean index 109a2417ec2c6..bf64d6c5dee03 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Composition.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Composition.lean @@ -98,8 +98,9 @@ theorem StableUnderInverse.unop {P : MorphismProperty Cᵒᵖ} (h : StableUnderI StableUnderInverse P.unop := fun _ _ e he => h e.op he #align category_theory.morphism_property.stable_under_inverse.unop CategoryTheory.MorphismProperty.StableUnderInverse.unop -theorem respectsIso_of_isStableUnderComposition {P : MorphismProperty C} [P.IsStableUnderComposition] - (hP : isomorphisms C ⊆ P) : RespectsIso P := +theorem respectsIso_of_isStableUnderComposition {P : MorphismProperty C} + [P.IsStableUnderComposition] (hP : isomorphisms C ⊆ P) : + RespectsIso P := ⟨fun _ _ hf => P.comp_mem _ _ (hP _ (isomorphisms.infer_property _)) hf, fun _ _ hf => P.comp_mem _ _ hf (hP _ (isomorphisms.infer_property _))⟩ #align category_theory.morphism_property.stable_under_composition.respects_iso CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition From a24362a73affba758be377672aac4bc9ebdd0aee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 26 Apr 2024 22:58:42 +0200 Subject: [PATCH 09/15] fixed docstring --- Mathlib/CategoryTheory/MorphismProperty/Composition.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Mathlib/CategoryTheory/MorphismProperty/Composition.lean b/Mathlib/CategoryTheory/MorphismProperty/Composition.lean index bf64d6c5dee03..4f6cbc0266c06 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Composition.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Composition.lean @@ -10,10 +10,7 @@ import Mathlib.CategoryTheory.MorphismProperty.Basic Given `P : MorphismProperty C`, we define the predicate `P.IsStableUnderComposition` which means that `P f → P g → P (f ≫ g)`. We also introduce the type classes -`W.ContainsIdentities` and `W.IsMultiplicative`. - -## TODO -* define the type class of morphism properties that satisfy the 2-out-of-3 property +`W.ContainsIdentities`, `W.IsMultiplicative`, and `W.HasTwoOutOfThreeProperty`. -/ From b09608fd0411f274882b63bd69b6aa1a227180ab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 26 Apr 2024 23:02:04 +0200 Subject: [PATCH 10/15] fixing the build --- .../CategoryTheory/Localization/Construction.lean | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/Mathlib/CategoryTheory/Localization/Construction.lean b/Mathlib/CategoryTheory/Localization/Construction.lean index 36a5ebbd006ac..159c2ce8be1de 100644 --- a/Mathlib/CategoryTheory/Localization/Construction.lean +++ b/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 From d4d25a9aa4537860ce983bc8907d772af823dbb2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 26 Apr 2024 23:50:26 +0200 Subject: [PATCH 11/15] fixing the build --- .../Morphisms/OpenImmersion.lean | 14 ++-- .../Morphisms/QuasiCompact.lean | 7 +- .../Morphisms/RingHomProperties.lean | 84 +++++++++---------- .../Morphisms/UniversallyClosed.lean | 23 +++-- 4 files changed, 69 insertions(+), 59 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean b/Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean index 272cc98341fee..8cfb3b103b42d 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean +++ b/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 diff --git a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean index b7dbface48ada..693b75f6ab1e9 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean +++ b/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 diff --git a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean index ac5b5b92bba48..a6a1dd8812f0d 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean +++ b/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 diff --git a/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean b/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean index 6247403ae8e27..2e675d93f0a26 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean @@ -54,17 +54,26 @@ 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 +92,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 From a13b6b2c1da085811bc9d3e462f0bcb03e9bde0a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 26 Apr 2024 23:58:32 +0200 Subject: [PATCH 12/15] fixing the build --- .../AlgebraicGeometry/Morphisms/FiniteType.lean | 11 +++++------ .../Morphisms/QuasiSeparated.lean | 14 +++++++------- .../CategoryTheory/MorphismProperty/Limits.lean | 4 ++-- 3 files changed, 14 insertions(+), 15 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean b/Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean index 5d6a653e841f2..6ce41aa0d2af5 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean +++ b/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 - diff --git a/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean b/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean index 3ad223cf1d899..0512b44f6442d 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean +++ b/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 diff --git a/Mathlib/CategoryTheory/MorphismProperty/Limits.lean b/Mathlib/CategoryTheory/MorphismProperty/Limits.lean index 99b0e28be3c5d..9d42b75d552f8 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Limits.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Limits.lean @@ -228,12 +228,12 @@ theorem RespectsIso.diagonal (hP : P.RespectsIso) : P.diagonal.RespectsIso := by rwa [pullback.diagonal_comp, hP.cancel_right_isIso] #align category_theory.morphism_property.respects_iso.diagonal CategoryTheory.MorphismProperty.RespectsIso.diagonal -theorem StableUnderComposition.diagonal [P.IsStableUnderComposition] (hP' : RespectsIso P) +theorem diagonal_isStableUnderComposition [P.IsStableUnderComposition] (hP' : RespectsIso P) (hP'' : StableUnderBaseChange P) : P.diagonal.IsStableUnderComposition where comp_mem _ _ h₁ h₂ := by rw [diagonal_iff, pullback.diagonal_comp] exact P.comp_mem _ _ h₁ (by simpa [hP'.cancel_left_isIso] using hP''.snd _ _ h₂) -#align category_theory.morphism_property.stable_under_composition.diagonal CategoryTheory.MorphismProperty.StableUnderComposition.diagonal +#align category_theory.morphism_property.stable_under_composition.diagonal CategoryTheory.MorphismProperty.diagonal_isStableUnderComposition theorem StableUnderBaseChange.diagonal (hP : StableUnderBaseChange P) (hP' : RespectsIso P) : P.diagonal.StableUnderBaseChange := From 8d92967f367d345d45ece8a801c3162265f3f40c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sat, 27 Apr 2024 00:01:55 +0200 Subject: [PATCH 13/15] fixing long line --- Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean b/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean index 2e675d93f0a26..c5ae3d2f83014 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean @@ -58,7 +58,8 @@ 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 +instance universallyClosed_isStableUnderComposition : + IsStableUnderComposition @UniversallyClosed := by rw [universallyClosed_eq] infer_instance #align algebraic_geometry.universally_closed_stable_under_composition AlgebraicGeometry.universallyClosed_isStableUnderComposition From f7e9f543165b3c651707f37b96db49eba838b473 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Sun, 28 Apr 2024 10:58:01 +0200 Subject: [PATCH 14/15] Update Mathlib/CategoryTheory/MorphismProperty/Basic.lean Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com> --- Mathlib/CategoryTheory/MorphismProperty/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/MorphismProperty/Basic.lean b/Mathlib/CategoryTheory/MorphismProperty/Basic.lean index 21bd60143e71a..a15c9943ea655 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Basic.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Basic.lean @@ -100,7 +100,7 @@ def inverseImage (P : MorphismProperty D) (F : C ⥤ D) : MorphismProperty C := @[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 + 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 => From 70e66e284fffee799670ca2b10a7c41b0b5c0595 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sun, 28 Apr 2024 16:11:40 +0200 Subject: [PATCH 15/15] made IsStableUnderComposition.unop an instance --- Mathlib/CategoryTheory/MorphismProperty/Composition.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/MorphismProperty/Composition.lean b/Mathlib/CategoryTheory/MorphismProperty/Composition.lean index 4f6cbc0266c06..269ff118bd26c 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Composition.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Composition.lean @@ -76,7 +76,7 @@ instance IsStableUnderComposition.op {P : MorphismProperty C} [P.IsStableUnderCo comp_mem f g hf hg := P.comp_mem g.unop f.unop hg hf #align category_theory.morphism_property.stable_under_composition.op CategoryTheory.MorphismProperty.IsStableUnderComposition.op -theorem IsStableUnderComposition.unop {P : MorphismProperty Cᵒᵖ} [P.IsStableUnderComposition] : +instance IsStableUnderComposition.unop {P : MorphismProperty Cᵒᵖ} [P.IsStableUnderComposition] : P.unop.IsStableUnderComposition where comp_mem f g hf hg := P.comp_mem g.op f.op hg hf #align category_theory.morphism_property.stable_under_composition.unop CategoryTheory.MorphismProperty.IsStableUnderComposition.unop