diff --git a/Mathlib/Algebra/Homology/Localization.lean b/Mathlib/Algebra/Homology/Localization.lean index 8a38d8959446c..38e3785936f5f 100644 --- a/Mathlib/Algebra/Homology/Localization.lean +++ b/Mathlib/Algebra/Homology/Localization.lean @@ -89,9 +89,9 @@ variable (C : Type*) [Category C] {ι : Type*} (c : ComplexShape ι) [Preadditiv lemma HomologicalComplexUpToQuasiIso.Q_inverts_homotopyEquivalences : (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy HomologicalComplexUpToQuasiIso.Q := - MorphismProperty.IsInvertedBy.of_subset _ _ _ + MorphismProperty.IsInvertedBy.of_le _ _ _ (Localization.inverts Q (HomologicalComplex.quasiIso C c)) - (homotopyEquivalences_subset_quasiIso C c) + (homotopyEquivalences_le_quasiIso C c) namespace HomotopyCategory @@ -198,7 +198,7 @@ instance : HomologicalComplexUpToQuasiIso.Qh.IsLocalization (HomotopyCategory.qu Functor.IsLocalization.of_comp (HomotopyCategory.quotient C c) Qh (HomologicalComplex.homotopyEquivalences C c) (HomotopyCategory.quasiIso C c) (HomologicalComplex.quasiIso C c) - (homotopyEquivalences_subset_quasiIso C c) + (homotopyEquivalences_le_quasiIso C c) (HomotopyCategory.quasiIso_eq_quasiIso_map_quotient C c) end @@ -236,9 +236,9 @@ lemma ComplexShape.QFactorsThroughHomotopy_of_exists_prev [CategoryWithHomology areEqualizedByLocalization {K L f g} h := by have : DecidableRel c.Rel := by classical infer_instance exact h.map_eq_of_inverts_homotopyEquivalences hc _ - (MorphismProperty.IsInvertedBy.of_subset _ _ _ + (MorphismProperty.IsInvertedBy.of_le _ _ _ (Localization.inverts _ (HomologicalComplex.quasiIso C _)) - (homotopyEquivalences_subset_quasiIso C _)) + (homotopyEquivalences_le_quasiIso C _)) end Cylinder diff --git a/Mathlib/Algebra/Homology/QuasiIso.lean b/Mathlib/Algebra/Homology/QuasiIso.lean index de72b93cee7cc..421e05e10fd67 100644 --- a/Mathlib/Algebra/Homology/QuasiIso.lean +++ b/Mathlib/Algebra/Homology/QuasiIso.lean @@ -497,8 +497,8 @@ instance : QuasiIso e.inv := (inferInstance : QuasiIso e.symm.hom) variable (C c) -lemma homotopyEquivalences_subset_quasiIso [CategoryWithHomology C] : - homotopyEquivalences C c ⊆ quasiIso C c := by +lemma homotopyEquivalences_le_quasiIso [CategoryWithHomology C] : + homotopyEquivalences C c ≤ quasiIso C c := by rintro K L _ ⟨e, rfl⟩ simp only [HomologicalComplex.mem_quasiIso_iff] infer_instance diff --git a/Mathlib/CategoryTheory/Localization/Composition.lean b/Mathlib/CategoryTheory/Localization/Composition.lean index ad6cdbd639b37..ad904eda0105d 100644 --- a/Mathlib/CategoryTheory/Localization/Composition.lean +++ b/Mathlib/CategoryTheory/Localization/Composition.lean @@ -34,11 +34,11 @@ def StrictUniversalPropertyFixedTarget.comp (h₁ : StrictUniversalPropertyFixedTarget L₁ W₁ E) (h₂ : StrictUniversalPropertyFixedTarget L₂ W₂ E) (W₃ : MorphismProperty C₁) (hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)) - (hW₁₃ : W₁ ⊆ W₃) (hW₂₃ : W₂ ⊆ W₃.map L₁) : + (hW₁₃ : W₁ ≤ W₃) (hW₂₃ : W₂ ≤ W₃.map L₁) : StrictUniversalPropertyFixedTarget (L₁ ⋙ L₂) W₃ E where inverts := hW₃ - lift F hF := h₂.lift (h₁.lift F (MorphismProperty.IsInvertedBy.of_subset _ _ F hF hW₁₃)) (by - refine' MorphismProperty.IsInvertedBy.of_subset _ _ _ _ hW₂₃ + lift F hF := h₂.lift (h₁.lift F (MorphismProperty.IsInvertedBy.of_le _ _ F hF hW₁₃)) (by + refine' MorphismProperty.IsInvertedBy.of_le _ _ _ _ hW₂₃ simpa only [MorphismProperty.IsInvertedBy.map_iff, h₁.fac F] using hF) fac F hF := by rw [Functor.assoc, h₂.fac, h₁.fac] uniq F₁ F₂ h := h₂.uniq _ _ (h₁.uniq _ _ (by simpa only [Functor.assoc] using h)) @@ -55,7 +55,7 @@ variable (L₁ W₁ L₂ W₂) lemma comp [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] (W₃ : MorphismProperty C₁) (hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)) - (hW₁₃ : W₁ ⊆ W₃) (hW₂₃ : W₂ ⊆ W₃.map L₁) : + (hW₁₃ : W₁ ≤ W₃) (hW₂₃ : W₂ ≤ W₃.map L₁) : (L₁ ⋙ L₂).IsLocalization W₃ := by -- The proof proceeds by reducing to the case of the constructed -- localized categories, which satisfy the strict universal property @@ -74,7 +74,7 @@ lemma comp [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] W₂.isoClosure_respectsIso E₂.functor rw [MorphismProperty.map_isoClosure] at eq rw [eq] - apply W₂.subset_isoClosure } + apply W₂.le_isoClosure } have := LocalizerMorphism.IsLocalizedEquivalence.of_equivalence Φ (by rfl) -- The fact that `Φ` is a localized equivalence allows to consider -- the induced equivalence of categories `E₃ : C₃ ≅ W₂'.Localization`, and @@ -94,9 +94,9 @@ lemma comp [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] have hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q) := by simpa only [← MorphismProperty.IsInvertedBy.iff_comp _ _ E₃.inverse, MorphismProperty.IsInvertedBy.iff_of_iso W₃ iso] using hW₃ - have hW₂₃' : W₂' ⊆ W₃.map W₁.Q := (MorphismProperty.monotone_map _ _ E₂.functor hW₂₃).trans + have hW₂₃' : W₂' ≤ W₃.map W₁.Q := (MorphismProperty.monotone_map E₂.functor hW₂₃).trans (by simpa only [W₃.map_map] - using subset_of_eq (W₃.map_eq_of_iso (compUniqFunctor L₁ W₁.Q W₁))) + using le_of_eq (W₃.map_eq_of_iso (compUniqFunctor L₁ W₁.Q W₁))) have : (W₁.Q ⋙ W₂'.Q).IsLocalization W₃ := by refine' IsLocalization.mk' _ _ _ _ all_goals @@ -108,7 +108,7 @@ lemma comp [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] lemma of_comp (W₃ : MorphismProperty C₁) [L₁.IsLocalization W₁] [(L₁ ⋙ L₂).IsLocalization W₃] - (hW₁₃ : W₁ ⊆ W₃) (hW₂₃ : W₂ = W₃.map L₁) : + (hW₁₃ : W₁ ≤ W₃) (hW₂₃ : W₂ = W₃.map L₁) : L₂.IsLocalization W₂ := by have : (L₁ ⋙ W₂.Q).IsLocalization W₃ := comp L₁ W₂.Q W₁ W₂ W₃ (fun X Y f hf => Localization.inverts W₂.Q W₂ _ diff --git a/Mathlib/CategoryTheory/Localization/Equivalence.lean b/Mathlib/CategoryTheory/Localization/Equivalence.lean index d3f94bed50baa..3f08956dc107d 100644 --- a/Mathlib/CategoryTheory/Localization/Equivalence.lean +++ b/Mathlib/CategoryTheory/Localization/Equivalence.lean @@ -66,7 +66,7 @@ the case of a functor `L₂ : C₂ ⥤ D` for a suitable `W₂ : MorphismPropert we have an equivalence of category `E : C₁ ≌ C₂` and an isomorphism `E.functor ⋙ L₂ ≅ L₁`. -/ lemma of_equivalence_source (L₁ : C₁ ⥤ D) (W₁ : MorphismProperty C₁) (L₂ : C₂ ⥤ D) (W₂ : MorphismProperty C₂) - (E : C₁ ≌ C₂) (hW₁ : W₁ ⊆ W₂.isoClosure.inverseImage E.functor) (hW₂ : W₂.IsInvertedBy L₂) + (E : C₁ ≌ C₂) (hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor) (hW₂ : W₂.IsInvertedBy L₂) [L₁.IsLocalization W₁] (iso : E.functor ⋙ L₂ ≅ L₁) : L₂.IsLocalization W₂ := by have h : W₁.IsInvertedBy (E.functor ⋙ W₂.Q) := fun _ _ f hf => by obtain ⟨_, _, f', hf', ⟨e⟩⟩ := hW₁ f hf @@ -99,7 +99,7 @@ a suitable `W₂ : MorphismProperty C₂`. -/ lemma of_equivalences (L₁ : C₁ ⥤ D₁) (W₁ : MorphismProperty C₁) [L₁.IsLocalization W₁] (L₂ : C₂ ⥤ D₂) (W₂ : MorphismProperty C₂) (E : C₁ ≌ C₂) (E' : D₁ ≌ D₂) [CatCommSq E.functor L₁ L₂ E'.functor] - (hW₁ : W₁ ⊆ W₂.isoClosure.inverseImage E.functor) (hW₂ : W₂.IsInvertedBy L₂) : + (hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor) (hW₂ : W₂.IsInvertedBy L₂) : L₂.IsLocalization W₂ := by haveI : (E.functor ⋙ L₂).IsLocalization W₁ := of_equivalence_target L₁ W₁ _ E' ((CatCommSq.iso _ _ _ _).symm) diff --git a/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean b/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean index 04d9da712cef6..df1206087632c 100644 --- a/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean +++ b/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean @@ -42,7 +42,7 @@ structure LocalizerMorphism where /-- a functor between the two categories -/ functor : C₁ ⥤ C₂ /-- the functor is compatible with the `MorphismProperty` -/ - map : W₁ ⊆ W₂.inverseImage functor + map : W₁ ≤ W₂.inverseImage functor namespace LocalizerMorphism @@ -157,7 +157,7 @@ lemma IsLocalizedEquivalence.of_isLocalization_of_isLocalization an equivalence of categories and that `W₁` and `W₂` essentially correspond to each other via this equivalence, then `Φ` is a localized equivalence. -/ lemma IsLocalizedEquivalence.of_equivalence [Φ.functor.IsEquivalence] - (h : W₂ ⊆ W₁.map Φ.functor) : IsLocalizedEquivalence Φ := by + (h : W₂ ≤ W₁.map Φ.functor) : IsLocalizedEquivalence Φ := by haveI : Functor.IsLocalization (Φ.functor ⋙ MorphismProperty.Q W₂) W₁ := by refine' Functor.IsLocalization.of_equivalence_source W₂.Q W₂ (Φ.functor ⋙ W₂.Q) W₁ (Functor.asEquivalence Φ.functor).symm _ (Φ.inverts W₂.Q) diff --git a/Mathlib/CategoryTheory/Localization/Pi.lean b/Mathlib/CategoryTheory/Localization/Pi.lean index 72cc12ff2667e..bb9945167e596 100644 --- a/Mathlib/CategoryTheory/Localization/Pi.lean +++ b/Mathlib/CategoryTheory/Localization/Pi.lean @@ -89,7 +89,7 @@ instance {J : Type} [Finite J] {C : Type u₁} {D : Type u₂} [Category.{v₁} refine Functor.IsLocalization.of_equivalences L₁ (MorphismProperty.pi (fun _ => W)) L₂ _ E E' ?_ ?_ · intro X Y f hf - exact MorphismProperty.subset_isoClosure _ _ (fun ⟨j⟩ => hf j) + exact MorphismProperty.le_isoClosure _ _ (fun ⟨j⟩ => hf j) · intro X Y f hf have : ∀ (j : Discrete J), IsIso ((L₂.map f).app j) := fun j => Localization.inverts L W _ (hf j) diff --git a/Mathlib/CategoryTheory/Localization/Predicate.lean b/Mathlib/CategoryTheory/Localization/Predicate.lean index 83c096efc714d..60119682a70a3 100644 --- a/Mathlib/CategoryTheory/Localization/Predicate.lean +++ b/Mathlib/CategoryTheory/Localization/Predicate.lean @@ -104,7 +104,7 @@ instance : Inhabited (StrictUniversalPropertyFixedTarget W.Q W E) := /-- When `W` consists of isomorphisms, the identity satisfies the universal property of the localization. -/ @[simps] -def strictUniversalPropertyFixedTargetId (hW : W ⊆ MorphismProperty.isomorphisms C) : +def strictUniversalPropertyFixedTargetId (hW : W ≤ MorphismProperty.isomorphisms C) : StrictUniversalPropertyFixedTarget (𝟭 C) W E where inverts X Y f hf := hW f hf @@ -147,7 +147,7 @@ theorem IsLocalization.mk' (h₁ : Localization.StrictUniversalPropertyFixedTarg rfl } } #align category_theory.functor.is_localization.mk' CategoryTheory.Functor.IsLocalization.mk' -theorem IsLocalization.for_id (hW : W ⊆ MorphismProperty.isomorphisms C) : (𝟭 C).IsLocalization W := +theorem IsLocalization.for_id (hW : W ≤ MorphismProperty.isomorphisms C) : (𝟭 C).IsLocalization W := IsLocalization.mk' _ _ (Localization.strictUniversalPropertyFixedTargetId W _ hW) (Localization.strictUniversalPropertyFixedTargetId W _ hW) #align category_theory.functor.is_localization.for_id CategoryTheory.Functor.IsLocalization.for_id @@ -442,7 +442,7 @@ theorem of_equivalence_target {E : Type*} [Category E] (L' : C ⥤ E) (eq : D #align category_theory.functor.is_localization.of_equivalence_target CategoryTheory.Functor.IsLocalization.of_equivalence_target lemma of_isEquivalence (L : C ⥤ D) (W : MorphismProperty C) - (hW : W ⊆ MorphismProperty.isomorphisms C) [IsEquivalence L] : + (hW : W ≤ MorphismProperty.isomorphisms C) [IsEquivalence L] : L.IsLocalization W := by haveI : (𝟭 C).IsLocalization W := for_id W hW exact of_equivalence_target (𝟭 C) W L L.asEquivalence L.leftUnitor diff --git a/Mathlib/CategoryTheory/MorphismProperty/Basic.lean b/Mathlib/CategoryTheory/MorphismProperty/Basic.lean index a15c9943ea655..93a6f748a7a1f 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Basic.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Basic.lean @@ -5,7 +5,7 @@ Authors: Andrew Yang -/ import Mathlib.CategoryTheory.Comma.Arrow import Mathlib.CategoryTheory.Pi.Basic -import Mathlib.Order.CompleteLattice +import Mathlib.Order.CompleteBooleanAlgebra #align_import category_theory.morphism_property from "leanprover-community/mathlib"@"7f963633766aaa3ebc8253100a5229dd463040c7" @@ -36,9 +36,12 @@ 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 : CompleteBooleanAlgebra (MorphismProperty C) where + le P₁ P₂ := ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P₁ f → P₂ f + __ := inferInstanceAs (CompleteBooleanAlgebra (∀ ⦃X Y : C⦄ (_ : X ⟶ Y), Prop)) + +lemma MorphismProperty.le_def {P Q : MorphismProperty C} : + P ≤ Q ↔ ∀ {X Y : C} (f : X ⟶ Y), P f → Q f := Iff.rfl instance : Inhabited (MorphismProperty C) := ⟨⊤⟩ @@ -55,26 +58,10 @@ lemma ext (W W' : MorphismProperty C) (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f funext X Y f rw [h] +@[simp] 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 @@ -109,9 +96,9 @@ def map (P : MorphismProperty C) (F : C ⥤ D) : MorphismProperty D := fun _ _ 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⟩⟩ +lemma monotone_map (F : C ⥤ D) : + Monotone (map · F) := by + intro P Q h 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 -/ @@ -132,7 +119,7 @@ theorem RespectsIso.unop {P : MorphismProperty Cᵒᵖ} (h : RespectsIso P) : Re 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 := +lemma le_isoClosure (P : MorphismProperty C) : P ≤ P.isoClosure := fun _ _ f hf => ⟨_, _, f, hf, ⟨Iso.refl _⟩⟩ lemma isoClosure_respectsIso (P : MorphismProperty C) : @@ -144,9 +131,8 @@ lemma isoClosure_respectsIso (P : MorphismProperty C) : ⟨_, _, 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⟩⟩ +lemma monotone_isoClosure : Monotone (isoClosure (C := C)) := by + intro P Q h 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} @@ -182,23 +168,26 @@ theorem RespectsIso.of_respects_arrow_iso (P : MorphismProperty C) 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) +lemma isoClosure_eq_iff {P : MorphismProperty C} : + P.isoClosure = P ↔ P.RespectsIso := by + refine ⟨(· ▸ P.isoClosure_respectsIso), fun hP ↦ le_antisymm ?_ (P.le_isoClosure)⟩ intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩ exact (hP.arrow_mk_iso_iff e).1 hf' +lemma RespectsIso.isoClosure_eq {P : MorphismProperty C} (hP : P.RespectsIso) : + P.isoClosure = P := by rwa [isoClosure_eq_iff] + @[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 +lemma isoClosure_le_iff (P Q : MorphismProperty C) (hQ : RespectsIso Q) : + P.isoClosure ≤ Q ↔ P ≤ Q := by constructor - · exact P.subset_isoClosure.trans + · exact P.le_isoClosure.trans · intro h - exact (monotone_isoClosure _ _ h).trans (by rw [hQ.isoClosure_eq]) + exact (monotone_isoClosure h).trans (by rw [hQ.isoClosure_eq]) lemma map_respectsIso (P : MorphismProperty C) (F : C ⥤ D) : (P.map F).RespectsIso := by @@ -206,30 +195,30 @@ lemma map_respectsIso (P : MorphismProperty C) (F : C ⥤ D) : 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 +lemma map_le_iff {P : MorphismProperty C} {F : C ⥤ D} {Q : MorphismProperty D} + (hQ : RespectsIso Q) : + P.map F ≤ Q ↔ P ≤ Q.inverseImage 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') + 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)] + apply le_antisymm + · rw [map_le_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) + · exact monotone_map _ (le_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] + apply le_antisymm + · rw [map_le_iff P.isoClosure_respectsIso] intro X Y f hf - exact P.subset_isoClosure _ hf + exact P.le_isoClosure _ hf · intro X Y f hf exact hf @@ -240,11 +229,11 @@ lemma map_id (P : MorphismProperty C) (hP : RespectsIso P) : @[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))] + apply le_antisymm + · rw [map_le_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)] + · rw [map_le_iff (map_respectsIso _ G)] intro X Y f hf exact map_mem_map _ _ _ (map_mem_map _ _ _ hf) @@ -261,23 +250,23 @@ theorem RespectsIso.inverseImage {P : MorphismProperty D} (h : RespectsIso P) (F 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 + 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 := +lemma map_inverseImage_le (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 + apply le_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)] + · rw [map_le_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 diff --git a/Mathlib/CategoryTheory/MorphismProperty/Composition.lean b/Mathlib/CategoryTheory/MorphismProperty/Composition.lean index 269ff118bd26c..0aae938d6ad66 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Composition.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Composition.lean @@ -96,7 +96,7 @@ theorem StableUnderInverse.unop {P : MorphismProperty Cᵒᵖ} (h : StableUnderI #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) : + [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 _))⟩ diff --git a/Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean b/Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean index 145dc072ca628..8a87db6ff6d61 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean @@ -34,7 +34,7 @@ def IsInvertedBy (P : MorphismProperty C) (F : C ⥤ D) : Prop := namespace IsInvertedBy -lemma of_subset (P Q : MorphismProperty C) (F : C ⥤ D) (hQ : Q.IsInvertedBy F) (h : P ⊆ Q) : +lemma of_le (P Q : MorphismProperty C) (F : C ⥤ D) (hQ : Q.IsInvertedBy F) (h : P ≤ Q) : P.IsInvertedBy F := fun _ _ _ hf => hQ _ (h _ hf) @@ -136,7 +136,7 @@ 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) + exact h _ (W.le_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] @@ -156,19 +156,17 @@ lemma IsInvertedBy.iff_comp {C₁ C₂ C₃ : Type*} [Category C₁] [Category C · 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.iff_le_inverseImage_isomorphisms (W : MorphismProperty C) (F : C ⥤ D) : + W.IsInvertedBy F ↔ W ≤ (isomorphisms D).inverseImage F := Iff.rfl + +lemma IsInvertedBy.iff_map_le_isomorphisms (W : MorphismProperty C) (F : C ⥤ D) : + W.IsInvertedBy F ↔ W.map F ≤ isomorphisms D := by + rw [iff_le_inverseImage_isomorphisms, map_le_iff (RespectsIso.isomorphisms D)] 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] + simp only [IsInvertedBy.iff_map_le_isomorphisms, map_map] end MorphismProperty diff --git a/Mathlib/CategoryTheory/MorphismProperty/Limits.lean b/Mathlib/CategoryTheory/MorphismProperty/Limits.lean index 9d42b75d552f8..dd72f14320d34 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Limits.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Limits.lean @@ -287,13 +287,17 @@ theorem universally_le (P : MorphismProperty C) : P.universally ≤ P := by 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 universally_eq_iff {P : MorphismProperty C} : + P.universally = P ↔ P.StableUnderBaseChange := + ⟨(· ▸ P.universally_stableUnderBaseChange), + fun hP ↦ P.universally_le.antisymm fun _ _ _ hf _ _ _ _ _ H => hP H.flip hf⟩ + theorem StableUnderBaseChange.universally_eq {P : MorphismProperty C} - (hP : P.StableUnderBaseChange) : P.universally = P := - P.universally_le.antisymm fun _ _ _ hf _ _ _ _ _ H => hP H.flip hf + (hP : P.StableUnderBaseChange) : P.universally = P := universally_eq_iff.mpr hP #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) + fun _ _ h _ _ _ h₁ _ _ _ _ _ H => h _ (h₁ _ _ _ H) #align category_theory.morphism_property.universally_mono CategoryTheory.MorphismProperty.universally_mono end Universally