From 2865aeda84135fad248864181270996cbf195fe2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 29 Aug 2023 15:10:23 +0000 Subject: [PATCH] feat: multiplicative morphism properties (#6698) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR introduces the notion of multiplicative morphism property, i.e. contains identities and is stable under composition. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> --- Mathlib/CategoryTheory/MorphismProperty.lean | 51 ++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/Mathlib/CategoryTheory/MorphismProperty.lean b/Mathlib/CategoryTheory/MorphismProperty.lean index 18256a7babf0a..31a34d7116ce5 100644 --- a/Mathlib/CategoryTheory/MorphismProperty.lean +++ b/Mathlib/CategoryTheory/MorphismProperty.lean @@ -695,6 +695,57 @@ theorem bijective_respectsIso : (MorphismProperty.bijective C).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 + end MorphismProperty end CategoryTheory