diff --git a/Mathlib.lean b/Mathlib.lean index 3435a680bbbdec..b1067bf455a4d7 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -7033,6 +7033,7 @@ public import Mathlib.Tactic.CategoryTheory.Coherence.Normalize public import Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence public import Mathlib.Tactic.CategoryTheory.Elementwise public import Mathlib.Tactic.CategoryTheory.IsoReassoc +public import Mathlib.Tactic.CategoryTheory.MkConcreteCategory public import Mathlib.Tactic.CategoryTheory.Monoidal.Basic public import Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes public import Mathlib.Tactic.CategoryTheory.Monoidal.Normalize diff --git a/Mathlib/Algebra/Category/AlgCat/Basic.lean b/Mathlib/Algebra/Category/AlgCat/Basic.lean index d60ab01c5aef1d..ed1390f1cf9d4f 100644 --- a/Mathlib/Algebra/Category/AlgCat/Basic.lean +++ b/Mathlib/Algebra/Category/AlgCat/Basic.lean @@ -57,60 +57,18 @@ lemma coe_of (X : Type v) [Ring X] [Algebra R X] : (of R X : Type v) = X := rfl variable {R} in -set_option backward.privateInPublic true in -/-- The type of morphisms in `AlgCat R`. -/ -@[ext] -structure Hom (A B : AlgCat.{v} R) where - private mk :: - /-- The underlying algebra map. -/ - hom' : A →ₐ[R] B - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category (AlgCat.{v} R) where - Hom A B := Hom A B - id A := ⟨AlgHom.id R A⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory (AlgCat.{v} R) (· →ₐ[R] ·) where - hom := Hom.hom' - ofHom := Hom.mk - -variable {R} in -/-- Turn a morphism in `AlgCat` back into an `AlgHom`. -/ -abbrev Hom.hom {A B : AlgCat.{v} R} (f : Hom A B) := - ConcreteCategory.hom (C := AlgCat R) f - -variable {R} in -/-- Typecheck an `AlgHom` as a morphism in `AlgCat`. -/ -abbrev ofHom {A B : Type v} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : - of R A ⟶ of R B := - ConcreteCategory.ofHom (C := AlgCat R) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (A B : AlgCat.{v} R) (f : Hom A B) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category (AlgCat.{v} R) (· →ₐ[R] ·) (AlgHom.id R) AlgHom.comp + with_of_hom {A B : Type v} [Ring A] [Ring B] [Algebra R A] [Algebra R B] + hom_type (A →ₐ[R] B) from (of R A) to (of R B) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ -@[simp] -lemma hom_id {A : AlgCat.{v} R} : (𝟙 A : A ⟶ A).hom = AlgHom.id R A := rfl - /- Provided for rewriting. -/ lemma id_apply (A : AlgCat.{v} R) (a : A) : (𝟙 A : A ⟶ A) a = a := by simp -@[simp] -lemma hom_comp {A B C : AlgCat.{v} R} (f : A ⟶ B) (g : B ⟶ C) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {A B C : AlgCat.{v} R} (f : A ⟶ B) (g : B ⟶ C) (a : A) : (f ≫ g) a = g (f a) := by simp @@ -119,14 +77,6 @@ lemma comp_apply {A B C : AlgCat.{v} R} (f : A ⟶ B) (g : B ⟶ C) (a : A) : lemma hom_ext {A B : AlgCat.{v} R} {f g : A ⟶ B} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Algebra R X] [Ring Y] - [Algebra R Y] (f : X →ₐ[R] Y) : (ofHom f).hom = f := rfl - -@[simp] -lemma ofHom_hom {A B : AlgCat.{v} R} (f : A ⟶ B) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {X : Type v} [Ring X] [Algebra R X] : ofHom (AlgHom.id R X) = 𝟙 (of R X) := rfl diff --git a/Mathlib/Algebra/Category/BoolRing.lean b/Mathlib/Algebra/Category/BoolRing.lean index 65a667b67ab649..c34d7209ecd927 100644 --- a/Mathlib/Algebra/Category/BoolRing.lean +++ b/Mathlib/Algebra/Category/BoolRing.lean @@ -51,39 +51,13 @@ theorem coe_of (α : Type*) [BooleanRing α] : ↥(of α) = α := instance : Inhabited BoolRing := ⟨of PUnit⟩ -variable {R} in -set_option backward.privateInPublic true in -/-- The type of morphisms in `BoolRing`. -/ -@[ext] -structure Hom (R S : BoolRing) where - private mk :: - /-- The underlying ring hom. -/ - hom' : R →+* S - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category BoolRing where - Hom R S := Hom R S - id R := ⟨RingHom.id R⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory BoolRing (· →+* ·) where - hom f := f.hom' - ofHom f := ⟨f⟩ - -/-- Turn a morphism in `BoolRing` back into a `RingHom`. -/ -abbrev Hom.hom {X Y : BoolRing} (f : Hom X Y) := - ConcreteCategory.hom (C := BoolRing) f - -/-- Typecheck a `RingHom` as a morphism in `BoolRing`. -/ -abbrev ofHom {R S : Type u} [BooleanRing R] [BooleanRing S] (f : R →+* S) : of R ⟶ of S := - ConcreteCategory.ofHom f +mk_concrete_category BoolRing.{u} (· →+* ·) RingHom.id RingHom.comp + with_of_hom {R S : Type u} [BooleanRing R] [BooleanRing S] + hom_type (R →+* S) from (of R) to (of S) @[ext] lemma hom_ext {R S : BoolRing} {f g : R ⟶ S} (hf : f.hom = g.hom) : f = g := - Hom.ext hf + ConcreteCategory.hom_ext f g <| RingHom.congr_fun hf instance hasForgetToCommRing : HasForget₂ BoolRing CommRingCat where forget₂ := @@ -95,8 +69,8 @@ set_option backward.privateInPublic.warn false in /-- Constructs an isomorphism of Boolean rings from a ring isomorphism between them. -/ @[simps] def Iso.mk {α β : BoolRing.{u}} (e : α ≃+* β) : α ≅ β where - hom := ⟨e⟩ - inv := ⟨e.symm⟩ + hom := ofHom e + inv := ofHom e.symm hom_inv_id := by ext; exact e.symm_apply_apply _ inv_hom_id := by ext; exact e.apply_symm_apply _ diff --git a/Mathlib/Algebra/Category/CommAlgCat/Basic.lean b/Mathlib/Algebra/Category/CommAlgCat/Basic.lean index 890af256ec28cc..0a5146f99ed543 100644 --- a/Mathlib/Algebra/Category/CommAlgCat/Basic.lean +++ b/Mathlib/Algebra/Category/CommAlgCat/Basic.lean @@ -57,57 +57,22 @@ abbrev of (X : Type v) [CommRing X] [Algebra R X] : CommAlgCat.{v} R := ⟨X⟩ variable (R) in lemma coe_of (X : Type v) [CommRing X] [Algebra R X] : (of R X : Type v) = X := rfl -set_option backward.privateInPublic true in -/-- The type of morphisms in `CommAlgCat R`. -/ -@[ext] -structure Hom (A B : CommAlgCat.{v} R) where - private mk :: - /-- The underlying algebra map. -/ - hom' : A →ₐ[R] B - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category (CommAlgCat.{v} R) where - Hom A B := Hom A B - id A := ⟨AlgHom.id R A⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory (CommAlgCat.{v} R) (· →ₐ[R] ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `CommAlgCat` back into an `AlgHom`. -/ -abbrev Hom.hom (f : Hom A B) := ConcreteCategory.hom (C := CommAlgCat R) f - -/-- Typecheck an `AlgHom` as a morphism in `CommAlgCat`. -/ -abbrev ofHom (f : X →ₐ[R] Y) : of R X ⟶ of R Y := ConcreteCategory.ofHom (C := CommAlgCat R) f - -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (A B : CommAlgCat.{v} R) (f : Hom A B) := f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category (CommAlgCat.{v} R) (· →ₐ[R] ·) (AlgHom.id R) AlgHom.comp + with_of_hom {X Y : Type v} [CommRing X] [Algebra R X] [CommRing Y] [Algebra R Y] + hom_type (X →ₐ[R] Y) from (of R X) to (of R Y) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ -@[simp] lemma hom_id : (𝟙 A : A ⟶ A).hom = AlgHom.id R A := rfl - /- Provided for rewriting. -/ lemma id_apply (A : CommAlgCat.{v} R) (a : A) : (𝟙 A : A ⟶ A) a = a := by simp -@[simp] lemma hom_comp (f : A ⟶ B) (g : B ⟶ C) : (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply (f : A ⟶ B) (g : B ⟶ C) (a : A) : (f ≫ g) a = g (f a) := by simp @[ext] lemma hom_ext {f g : A ⟶ B} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] lemma hom_ofHom (f : X →ₐ[R] Y) : (ofHom f).hom = f := rfl -@[simp] lemma ofHom_hom (f : A ⟶ B) : ofHom f.hom = f := rfl - @[simp] lemma ofHom_id : ofHom (.id R X) = 𝟙 (of R X) := rfl @[simp] diff --git a/Mathlib/Algebra/Category/CommBialgCat.lean b/Mathlib/Algebra/Category/CommBialgCat.lean index 285629a1cdc3f6..e5ac8f790d6209 100644 --- a/Mathlib/Algebra/Category/CommBialgCat.lean +++ b/Mathlib/Algebra/Category/CommBialgCat.lean @@ -59,55 +59,19 @@ abbrev of (X : Type v) [CommRing X] [Bialgebra R X] : CommBialgCat.{v} R := ⟨X variable (R) in lemma coe_of (X : Type v) [CommRing X] [Bialgebra R X] : (of R X : Type v) = X := rfl -set_option backward.privateInPublic true in -/-- The type of morphisms in `CommBialgCat R`. -/ -@[ext] -structure Hom (A B : CommBialgCat.{v} R) where - private mk :: - /-- The underlying bialgebra map. -/ - hom' : A →ₐc[R] B - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category (CommBialgCat.{v} R) where - Hom A B := Hom A B - id A := ⟨.id R A⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory (CommBialgCat.{v} R) (· →ₐc[R] ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `CommBialgCat` back into a `BialgHom`. -/ -abbrev Hom.hom (f : Hom A B) : A →ₐc[R] B := ConcreteCategory.hom (C := CommBialgCat R) f - -/-- Typecheck a `BialgHom` as a morphism in `CommBialgCat R`. -/ -abbrev ofHom {X Y : Type v} {_ : CommRing X} {_ : CommRing Y} {_ : Bialgebra R X} - {_ : Bialgebra R Y} (f : X →ₐc[R] Y) : of R X ⟶ of R Y := - ConcreteCategory.ofHom (C := CommBialgCat R) f - -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (A B : CommBialgCat.{v} R) (f : Hom A B) := f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category (CommBialgCat.{v} R) (· →ₐc[R] ·) (BialgHom.id R) BialgHom.comp + with_of_hom {X Y : Type v} [CommRing X] [Bialgebra R X] [CommRing Y] [Bialgebra R Y] + hom_type (X →ₐc[R] Y) from (of R X) to (of R Y) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ -@[simp] lemma hom_id : (𝟙 A : A ⟶ A).hom = .id R A := rfl -@[simp] lemma hom_comp (f : A ⟶ B) (g : B ⟶ C) : (f ≫ g).hom = g.hom.comp f.hom := rfl - lemma id_apply (A : CommBialgCat.{v} R) (a : A) : (𝟙 A : A ⟶ A) a = a := by simp lemma comp_apply (f : A ⟶ B) (g : B ⟶ C) (a : A) : (f ≫ g) a = g (f a) := by simp @[ext] lemma hom_ext {f g : A ⟶ B} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] lemma hom_ofHom (f : X →ₐc[R] Y) : (ofHom f).hom = f := rfl -@[simp] lemma ofHom_hom (f : A ⟶ B) : ofHom f.hom = f := rfl - @[simp] lemma ofHom_id : ofHom (.id R X) = 𝟙 (of R X) := rfl @[simp] diff --git a/Mathlib/Algebra/Category/Grp/Basic.lean b/Mathlib/Algebra/Category/Grp/Basic.lean index 3f1342fbd31449..0a943dc93a7b50 100644 --- a/Mathlib/Algebra/Category/Grp/Basic.lean +++ b/Mathlib/Algebra/Category/Grp/Basic.lean @@ -60,56 +60,16 @@ abbrev of (M : Type u) [Group M] : GrpCat := ⟨M⟩ end GrpCat -/-- The type of morphisms in `AddGrpCat R`. -/ -@[ext] -structure AddGrpCat.Hom (A B : AddGrpCat.{u}) where - private mk :: - /-- The underlying monoid homomorphism. -/ - hom' : A →+ B - -set_option backward.privateInPublic true in -/-- The type of morphisms in `GrpCat R`. -/ -@[to_additive, ext] -structure GrpCat.Hom (A B : GrpCat.{u}) where - private mk :: - /-- The underlying monoid homomorphism. -/ - hom' : A →* B +@[to_additive AddGrpCat] +mk_concrete_category GrpCat.{u} (· →* ·) MonoidHom.id MonoidHom.comp + with_of_hom {X Y : Type u} [Group X] [Group Y] + hom_type (X →* Y) from (GrpCat.of X) to (GrpCat.of Y) + to_additive AddGrpCat.{u} (· →+ ·) AddMonoidHom.id AddMonoidHom.comp + with_of_hom {X Y : Type u} [AddGroup X] [AddGroup Y] + hom_type (X →+ Y) from (AddGrpCat.of X) to (AddGrpCat.of Y) namespace GrpCat -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -@[to_additive] -instance : Category GrpCat.{u} where - Hom X Y := Hom X Y - id X := ⟨MonoidHom.id X⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -@[to_additive] -instance : ConcreteCategory GrpCat (· →* ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `GrpCat` back into a `MonoidHom`. -/ -@[to_additive /-- Turn a morphism in `AddGrpCat` back into an `AddMonoidHom`. -/] -abbrev Hom.hom {X Y : GrpCat.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := GrpCat) f - -/-- Typecheck a `MonoidHom` as a morphism in `GrpCat`. -/ -@[to_additive /-- Typecheck an `AddMonoidHom` as a morphism in `AddGrpCat`. -/] -abbrev ofHom {X Y : Type u} [Group X] [Group Y] (f : X →* Y) : of X ⟶ of Y := - ConcreteCategory.ofHom (C := GrpCat) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : GrpCat.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) -initialize_simps_projections AddGrpCat.Hom (hom' → hom) - /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ @@ -131,18 +91,11 @@ lemma ext {X Y : GrpCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := theorem coe_of (R : Type u) [Group R] : ↑(GrpCat.of R) = R := rfl -@[to_additive (attr := simp)] -lemma hom_id {X : GrpCat} : (𝟙 X : X ⟶ X).hom = MonoidHom.id X := rfl - /- Provided for rewriting. -/ @[to_additive] lemma id_apply (X : GrpCat) (x : X) : (𝟙 X : X ⟶ X) x = x := by simp -@[to_additive (attr := simp)] -lemma hom_comp {X Y T : GrpCat} (f : X ⟶ Y) (g : Y ⟶ T) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ @[to_additive] lemma comp_apply {X Y T : GrpCat} (f : X ⟶ Y) (g : Y ⟶ T) (x : X) : @@ -152,13 +105,6 @@ lemma comp_apply {X Y T : GrpCat} (f : X ⟶ Y) (g : Y ⟶ T) (x : X) : lemma hom_ext {X Y : GrpCat} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[to_additive (attr := simp)] -lemma hom_ofHom {R S : Type u} [Group R] [Group S] (f : R →* S) : (ofHom f).hom = f := rfl - -@[to_additive (attr := simp)] -lemma ofHom_hom {X Y : GrpCat} (f : X ⟶ Y) : - ofHom (Hom.hom f) = f := rfl - @[to_additive (attr := simp)] lemma ofHom_id {X : Type u} [Group X] : ofHom (MonoidHom.id X) = 𝟙 (of X) := rfl @@ -277,56 +223,16 @@ abbrev of (M : Type u) [CommGroup M] : CommGrpCat := ⟨M⟩ end CommGrpCat -/-- The type of morphisms in `AddCommGrpCat R`. -/ -@[ext] -structure AddCommGrpCat.Hom (A B : AddCommGrpCat.{u}) where - private mk :: - /-- The underlying monoid homomorphism. -/ - hom' : A →+ B - -set_option backward.privateInPublic true in -/-- The type of morphisms in `CommGrpCat R`. -/ -@[to_additive, ext] -structure CommGrpCat.Hom (A B : CommGrpCat.{u}) where - private mk :: - /-- The underlying monoid homomorphism. -/ - hom' : A →* B +@[to_additive AddCommGrpCat] +mk_concrete_category CommGrpCat.{u} (· →* ·) MonoidHom.id MonoidHom.comp + with_of_hom {X Y : Type u} [CommGroup X] [CommGroup Y] + hom_type (X →* Y) from (CommGrpCat.of X) to (CommGrpCat.of Y) + to_additive AddCommGrpCat.{u} (· →+ ·) AddMonoidHom.id AddMonoidHom.comp + with_of_hom {X Y : Type u} [AddCommGroup X] [AddCommGroup Y] + hom_type (X →+ Y) from (AddCommGrpCat.of X) to (AddCommGrpCat.of Y) namespace CommGrpCat -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -@[to_additive] -instance : Category CommGrpCat.{u} where - Hom X Y := Hom X Y - id X := ⟨MonoidHom.id X⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -@[to_additive] -instance : ConcreteCategory CommGrpCat (· →* ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `CommGrpCat` back into a `MonoidHom`. -/ -@[to_additive /-- Turn a morphism in `AddCommGrpCat` back into an `AddMonoidHom`. -/] -abbrev Hom.hom {X Y : CommGrpCat.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := CommGrpCat) f - -/-- Typecheck a `MonoidHom` as a morphism in `CommGrpCat`. -/ -@[to_additive /-- Typecheck an `AddMonoidHom` as a morphism in `AddCommGrpCat`. -/] -abbrev ofHom {X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) : of X ⟶ of Y := - ConcreteCategory.ofHom (C := CommGrpCat) f - -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -@[to_additive /-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/] -def Hom.Simps.hom (X Y : CommGrpCat.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) -initialize_simps_projections AddCommGrpCat.Hom (hom' → hom) - /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ @@ -352,18 +258,11 @@ instance : Inhabited CommGrpCat := theorem coe_of (R : Type u) [CommGroup R] : ↑(CommGrpCat.of R) = R := rfl -@[to_additive (attr := simp)] -lemma hom_id {X : CommGrpCat} : (𝟙 X : X ⟶ X).hom = MonoidHom.id X := rfl - /- Provided for rewriting. -/ @[to_additive] lemma id_apply (X : CommGrpCat) (x : X) : (𝟙 X : X ⟶ X) x = x := by simp -@[to_additive (attr := simp)] -lemma hom_comp {X Y T : CommGrpCat} (f : X ⟶ Y) (g : Y ⟶ T) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ @[to_additive] lemma comp_apply {X Y T : CommGrpCat} (f : X ⟶ Y) (g : Y ⟶ T) (x : X) : @@ -373,13 +272,6 @@ lemma comp_apply {X Y T : CommGrpCat} (f : X ⟶ Y) (g : Y ⟶ T) (x : X) : lemma hom_ext {X Y : CommGrpCat} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[to_additive (attr := simp)] -lemma hom_ofHom {X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) : (ofHom f).hom = f := rfl - -@[to_additive (attr := simp)] -lemma ofHom_hom {X Y : CommGrpCat} (f : X ⟶ Y) : - ofHom (Hom.hom f) = f := rfl - @[to_additive (attr := simp)] lemma ofHom_id {X : Type u} [CommGroup X] : ofHom (MonoidHom.id X) = 𝟙 (of X) := rfl @@ -483,7 +375,7 @@ def asHom {G : AddCommGrpCat.{0}} (g : G) : AddCommGrpCat.of ℤ ⟶ G := ofHom (zmultiplesHom G g) theorem asHom_injective {G : AddCommGrpCat.{0}} : Function.Injective (@asHom G) := fun h k w => by - simpa using CategoryTheory.congr_fun w 1 + simpa [asHom] using ConcreteCategory.congr_hom w 1 @[ext] theorem int_hom_ext {G : AddCommGrpCat.{0}} (f g : AddCommGrpCat.of ℤ ⟶ G) @@ -494,7 +386,10 @@ theorem int_hom_ext {G : AddCommGrpCat.{0}} (f g : AddCommGrpCat.of ℤ ⟶ G) -- the forgetful functor is representable. theorem injective_of_mono {G H : AddCommGrpCat.{0}} (f : G ⟶ H) [Mono f] : Function.Injective f := fun g₁ g₂ h => by - have t0 : asHom g₁ ≫ f = asHom g₂ ≫ f := by cat_disch + have t0 : asHom g₁ ≫ f = asHom g₂ ≫ f := by + ext + change f ((asHom g₁) (1 : ℤ)) = f ((asHom g₂) (1 : ℤ)) + simp [asHom, h] have t1 : asHom g₁ = asHom g₂ := (cancel_mono _).1 t0 apply asHom_injective t1 diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index dca2a34dfc312a..7e703bf708350e 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -84,74 +84,35 @@ lemma coe_of (X : Type v) [Ring X] [Module R X] : (of R X : Type v) = X := example (X : Type v) [Ring X] [Module R X] : (of R X : Type v) = X := by with_reducible rfl example (M : ModuleCat.{v} R) : of R M = M := by with_reducible rfl -set_option backward.privateInPublic true in variable {R} in -/-- The type of morphisms in `ModuleCat R`. -/ -@[ext] -structure Hom (M N : ModuleCat.{v} R) where - private mk :: - /-- The underlying linear map. -/ - hom' : M →ₗ[R] N - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance moduleCategory : Category.{v, max (v + 1) u} (ModuleCat.{v} R) where - Hom M N := Hom M N - id _ := ⟨LinearMap.id⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory (ModuleCat.{v} R) (· →ₗ[R] ·) where - hom := Hom.hom' - ofHom := Hom.mk +mk_concrete_category (ModuleCat.{v} R) (· →ₗ[R] ·) (@LinearMap.id R ·) (LinearMap.comp · ·) + with_of_hom {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] + hom_type (X →ₗ[R] Y) from (of R X) to (of R Y) section variable {R} -/-- Turn a morphism in `ModuleCat` back into a `LinearMap`. -/ -abbrev Hom.hom {A B : ModuleCat.{v} R} (f : Hom A B) := - ConcreteCategory.hom (C := ModuleCat R) f - -/-- Typecheck a `LinearMap` as a morphism in `ModuleCat`. -/ -abbrev ofHom {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] - (f : X →ₗ[R] Y) : of R X ⟶ of R Y := - ConcreteCategory.ofHom (C := ModuleCat R) f - -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (A B : ModuleCat.{v} R) (f : Hom A B) := - f.hom - -initialize_simps_projections Hom (hom' → hom) - /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ -@[simp] -lemma hom_id {M : ModuleCat.{v} R} : (𝟙 M : M ⟶ M).hom = LinearMap.id := rfl - /- Provided for rewriting. -/ lemma id_apply (M : ModuleCat.{v} R) (x : M) : (𝟙 M : M ⟶ M) x = x := by simp -@[simp] -lemma hom_comp {M N O : ModuleCat.{v} R} (f : M ⟶ N) (g : N ⟶ O) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {M N O : ModuleCat.{v} R} (f : M ⟶ N) (g : N ⟶ O) (x : M) : (f ≫ g) x = g (f x) := by simp @[ext] lemma hom_ext {M N : ModuleCat.{v} R} {f g : M ⟶ N} (hf : f.hom = g.hom) : f = g := - Hom.ext hf + ConcreteCategory.hom_ext f g <| LinearMap.congr_fun hf lemma hom_bijective {M N : ModuleCat.{v} R} : Function.Bijective (Hom.hom : (M ⟶ N) → (M →ₗ[R] N)) where - left f g h := by cases f; cases g; simpa using h - right f := ⟨⟨f⟩, rfl⟩ + left _ _ h := hom_ext h + right f := ⟨ofHom f, by simp [Hom.hom]⟩ /-- Convenience shortcut for `ModuleCat.hom_bijective.injective`. -/ lemma hom_injective {M N : ModuleCat.{v} R} : @@ -163,14 +124,6 @@ lemma hom_surjective {M N : ModuleCat.{v} R} : Function.Surjective (Hom.hom : (M ⟶ N) → (M →ₗ[R] N)) := hom_bijective.surjective -@[simp] -lemma hom_ofHom {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] - [Module R Y] (f : X →ₗ[R] Y) : (ofHom f).hom = f := rfl - -@[simp] -lemma ofHom_hom {M N : ModuleCat.{v} R} (f : M ⟶ N) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {M : Type v} [AddCommGroup M] [Module R M] : ofHom LinearMap.id = 𝟙 (of R M) := rfl @@ -208,8 +161,12 @@ def equivalenceSemimoduleCat : ModuleCat.{v} R ≌ SemimoduleCat.{v} R where inverse := letI := Module.addCommMonoidToAddCommGroup { obj M := of R M map {M N} f := ofHom f.hom } - unitIso := NatIso.ofComponents fun _ ↦ { hom := ⟨.id⟩, inv := ⟨.id⟩ } - counitIso := NatIso.ofComponents fun _ ↦ { hom := ⟨.id⟩, inv := ⟨.id⟩ } + unitIso := NatIso.ofComponents fun _ ↦ + { hom := by refine ConcreteCategory.ofHom (C := ModuleCat R) ?_; exact LinearMap.id + inv := by refine ConcreteCategory.ofHom (C := ModuleCat R) ?_; exact LinearMap.id } + counitIso := NatIso.ofComponents fun _ ↦ + { hom := by refine ConcreteCategory.ofHom (C := SemimoduleCat R) ?_; exact LinearMap.id + inv := by refine ConcreteCategory.ofHom (C := SemimoduleCat R) ?_; exact LinearMap.id } end diff --git a/Mathlib/Algebra/Category/ModuleCat/Semi.lean b/Mathlib/Algebra/Category/ModuleCat/Semi.lean index 0e9b0a944f890d..cc3154c93d4ebe 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Semi.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Semi.lean @@ -83,68 +83,34 @@ example (X : Type v) [Semiring X] [Module R X] : (of R X : Type v) = X := by wit example (M : SemimoduleCat.{v} R) : of R M = M := by with_reducible rfl variable {R} in -/-- The type of morphisms in `SemimoduleCat R`. -/ -@[ext] -structure Hom (M N : SemimoduleCat.{v} R) where - mk :: - /-- The underlying linear map. -/ - hom' : M →ₗ[R] N - -instance moduleCategory : Category.{v, max (v + 1) u} (SemimoduleCat.{v} R) where - Hom M N := Hom M N - id _ := ⟨LinearMap.id⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -instance : ConcreteCategory (SemimoduleCat.{v} R) (· →ₗ[R] ·) where - hom := Hom.hom' - ofHom := Hom.mk +mk_concrete_category (SemimoduleCat.{v} R) (· →ₗ[R] ·) (@LinearMap.id R ·) LinearMap.comp + with_of_hom {X Y : Type v} [AddCommMonoid X] [Module R X] [AddCommMonoid Y] [Module R Y] + hom_type (X →ₗ[R] Y) from (of R X) to (of R Y) section variable {R} -/-- Turn a morphism in `SemimoduleCat` back into a `LinearMap`. -/ -abbrev Hom.hom {A B : SemimoduleCat.{v} R} (f : Hom A B) := - ConcreteCategory.hom (C := SemimoduleCat R) f - -/-- Typecheck a `LinearMap` as a morphism in `SemimoduleCat`. -/ -abbrev ofHom {X Y : Type v} [AddCommMonoid X] [Module R X] [AddCommMonoid Y] [Module R Y] - (f : X →ₗ[R] Y) : of R X ⟶ of R Y := - ConcreteCategory.ofHom (C := SemimoduleCat R) f - -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (A B : SemimoduleCat.{v} R) (f : Hom A B) := - f.hom - -initialize_simps_projections Hom (hom' → hom) - /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ -@[simp] -lemma hom_id {M : SemimoduleCat.{v} R} : (𝟙 M : M ⟶ M).hom = LinearMap.id := rfl - /- Provided for rewriting. -/ lemma id_apply (M : SemimoduleCat.{v} R) (x : M) : (𝟙 M : M ⟶ M) x = x := by simp -@[simp] -lemma hom_comp {M N O : SemimoduleCat.{v} R} (f : M ⟶ N) (g : N ⟶ O) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {M N O : SemimoduleCat.{v} R} (f : M ⟶ N) (g : N ⟶ O) (x : M) : (f ≫ g) x = g (f x) := by simp @[ext] lemma hom_ext {M N : SemimoduleCat.{v} R} {f g : M ⟶ N} (hf : f.hom = g.hom) : f = g := - Hom.ext hf + ConcreteCategory.hom_ext f g <| LinearMap.congr_fun hf lemma hom_bijective {M N : SemimoduleCat.{v} R} : Function.Bijective (Hom.hom : (M ⟶ N) → (M →ₗ[R] N)) where - left f g h := by cases f; cases g; simpa using h - right f := ⟨⟨f⟩, rfl⟩ + left _ _ h := hom_ext h + right f := ⟨ofHom f, by simp [Hom.hom]⟩ /-- Convenience shortcut for `SemimoduleCat.hom_bijective.injective`. -/ lemma hom_injective {M N : SemimoduleCat.{v} R} : @@ -156,14 +122,6 @@ lemma hom_surjective {M N : SemimoduleCat.{v} R} : Function.Surjective (Hom.hom : (M ⟶ N) → (M →ₗ[R] N)) := hom_bijective.surjective -@[simp] -lemma hom_ofHom {X Y : Type v} [AddCommMonoid X] [Module R X] [AddCommMonoid Y] - [Module R Y] (f : X →ₗ[R] Y) : (ofHom f).hom = f := rfl - -@[simp] -lemma ofHom_hom {M N : SemimoduleCat.{v} R} (f : M ⟶ N) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {M : Type v} [AddCommMonoid M] [Module R M] : ofHom LinearMap.id = 𝟙 (of R M) := rfl @@ -285,26 +243,32 @@ section AddCommMonoid variable {M N : SemimoduleCat.{v} R} instance : Add (M ⟶ N) where - add f g := ⟨f.hom + g.hom⟩ + add f g := ofHom (f.hom + g.hom) -@[simp] lemma hom_add (f g : M ⟶ N) : (f + g).hom = f.hom + g.hom := rfl +@[simp] lemma hom_add (f g : M ⟶ N) : (f + g).hom = f.hom + g.hom := by + change (ofHom (f.hom + g.hom)).hom = f.hom + g.hom + simp instance : Zero (M ⟶ N) where - zero := ⟨0⟩ + zero := ofHom 0 -@[simp] lemma hom_zero : (0 : M ⟶ N).hom = 0 := rfl +@[simp] lemma hom_zero : (0 : M ⟶ N).hom = 0 := by + change (ofHom (0 : M →ₗ[R] N)).hom = 0 + simp instance : SMul ℕ (M ⟶ N) where - smul n f := ⟨n • f.hom⟩ + smul n f := ofHom (n • f.hom) -@[simp] lemma hom_nsmul (n : ℕ) (f : M ⟶ N) : (n • f).hom = n • f.hom := rfl +lemma hom_nsmul (n : ℕ) (f : M ⟶ N) : (n • f).hom = n • f.hom := by + change (ofHom (n • f.hom)).hom = n • f.hom + simp -- There is no `ℤ`-smul operation on a general semimodule! @[deprecated (since := "2026-01-06")] alias hom_zsmul := hom_nsmul instance : AddCommMonoid (M ⟶ N) := - Function.Injective.addCommMonoid Hom.hom hom_injective rfl (fun _ _ => rfl) (fun _ _ => rfl) + Function.Injective.addCommMonoid Hom.hom hom_injective hom_zero hom_add (fun f n => hom_nsmul n f) @[simp] lemma hom_sum {ι : Type*} (f : ι → (M ⟶ N)) (s : Finset ι) : (∑ i ∈ s, f i).hom = ∑ i ∈ s, (f i).hom := @@ -321,7 +285,7 @@ instance : HasZeroMorphisms (SemimoduleCat.{v} R) where @[simps!] def homAddEquiv : (M ⟶ N) ≃+ (M →ₗ[R] N) := { homEquiv with - map_add' := fun _ _ => rfl } + map_add' := hom_add } theorem subsingleton_of_isZero (h : IsZero M) : Subsingleton M := by refine subsingleton_of_forall_eq 0 (fun x ↦ ?_) @@ -344,9 +308,11 @@ variable {M N : SemimoduleCat.{v} R} variable {S : Type*} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] instance : SMul S (M ⟶ N) where - smul c f := ⟨c • f.hom⟩ + smul c f := ofHom (c • f.hom) -@[simp] lemma hom_smul (s : S) (f : M ⟶ N) : (s • f).hom = s • f.hom := rfl +@[simp] lemma hom_smul (s : S) (f : M ⟶ N) : (s • f).hom = s • f.hom := by + change (ofHom (s • f.hom)).hom = s • f.hom + simp end SMul @@ -358,13 +324,13 @@ instance Hom.instModule : Module S (M ⟶ N) := Function.Injective.module S { toFun := Hom.hom, map_zero' := hom_zero, map_add' := hom_add } hom_injective - (fun _ _ => rfl) + hom_smul /-- `SemimoduleCat.Hom.hom` bundled as a linear equivalence. -/ @[simps] def homLinearEquiv : (M ⟶ N) ≃ₗ[S] (M →ₗ[R] N) := { homAddEquiv with - map_smul' := fun _ _ => rfl } + map_smul' := hom_smul } end Module @@ -408,11 +374,11 @@ instance : Linear S (SemimoduleCat.{v} S) := SemimoduleCat.Algebra.instLinear -/ variable {X Y X' Y' : SemimoduleCat.{v} S} theorem Iso.homCongr_eq_arrowCongr (i : X ≅ X') (j : Y ≅ Y') (f : X ⟶ Y) : - Iso.homCongr i j f = ⟨LinearEquiv.arrowCongr i.toLinearEquivₛ j.toLinearEquivₛ f.hom⟩ := + Iso.homCongr i j f = ofHom (LinearEquiv.arrowCongr i.toLinearEquivₛ j.toLinearEquivₛ f.hom) := rfl theorem Iso.conj_eq_conj (i : X ≅ X') (f : End X) : - Iso.conj i f = ⟨LinearEquiv.conj i.toLinearEquivₛ f.hom⟩ := + Iso.conj i f = ofHom (LinearEquiv.conj i.toLinearEquivₛ f.hom) := rfl end @@ -455,10 +421,14 @@ def Hom.hom₂ {M N P : SemimoduleCat.{u} R} (f : M ⟶ (of R (N ⟶ P))) : M (f ≫ ofHom homLinearEquiv.toLinearMap).hom @[simp] lemma Hom.hom₂_ofHom₂ {M N P : SemimoduleCat.{u} R} (f : M →ₗ[R] N →ₗ[R] P) : - (ofHom₂ f).hom₂ = f := rfl + (ofHom₂ f).hom₂ = f := by + ext x y + simp [ofHom₂, Hom.hom₂] @[simp] lemma ofHom₂_hom₂ {M N P : SemimoduleCat.{u} R} (f : M ⟶ of R (N ⟶ P)) : - ofHom₂ f.hom₂ = f := rfl + ofHom₂ f.hom₂ = f := by + ext x y + simp [ofHom₂, Hom.hom₂] end SemimoduleCat diff --git a/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean index b628050da40e5a..53656113dd671b 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean @@ -59,60 +59,13 @@ abbrev of (M : Type v) [AddCommGroup M] [Module R M] [TopologicalSpace M] [Conti lemma coe_of (M : Type v) [AddCommGroup M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul R M] : (of R M) = M := rfl -set_option backward.privateInPublic true in -variable {R} in -/-- Homs in `TopModuleCat` as one field structures over `ContinuousLinearMap`. -/ -structure Hom (X Y : TopModuleCat.{v} R) where - -- use `ofHom` instead - private ofHom' :: - /-- The underlying continuous linear map. Use `hom` instead. -/ - hom' : X →L[R] Y - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category (TopModuleCat R) where - Hom := Hom - id M := ⟨ContinuousLinearMap.id R M⟩ - comp φ ψ := ⟨ψ.hom' ∘L φ.hom'⟩ - -set_option linter.style.whitespace false in -- manual alignment is not recognised -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory (TopModuleCat R) (· →L[R] ·) where - hom := Hom.hom' - ofHom := Hom.ofHom' - variable {R} in -/-- Cast a hom in `TopModuleCat` into a continuous linear map. -/ -abbrev Hom.hom {X Y : TopModuleCat R} (f : X.Hom Y) : X →L[R] Y := - ConcreteCategory.hom (C := TopModuleCat R) f - -variable {R} in -/-- Construct a hom in `TopModuleCat` from a continuous linear map. -/ -abbrev ofHom {X Y : Type v} +mk_concrete_category (TopModuleCat.{v} R) (· →L[R] ·) + (fun (M : TopModuleCat.{v} R) ↦ ContinuousLinearMap.id R M) ContinuousLinearMap.comp + with_of_hom {X Y : Type v} [AddCommGroup X] [Module R X] [TopologicalSpace X] [ContinuousAdd X] [ContinuousSMul R X] [AddCommGroup Y] [Module R Y] [TopologicalSpace Y] [ContinuousAdd Y] [ContinuousSMul R Y] - (f : X →L[R] Y) : of R X ⟶ of R Y := - ConcreteCategory.ofHom f - -@[simp] lemma hom_ofHom {X Y : Type v} - [AddCommGroup X] [Module R X] [TopologicalSpace X] [ContinuousAdd X] [ContinuousSMul R X] - [AddCommGroup Y] [Module R Y] [TopologicalSpace Y] [ContinuousAdd Y] [ContinuousSMul R Y] - (f : X →L[R] Y) : - (ofHom f).hom = f := rfl - -@[simp] lemma ofHom_hom {X Y : TopModuleCat R} (f : X.Hom Y) : ofHom f.hom = f := rfl - -@[simp] lemma hom_comp {X Y Z : TopModuleCat R} (f : X ⟶ Y) (g : Y ⟶ Z) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - -@[simp] lemma hom_id (X : TopModuleCat R) : hom (𝟙 X) = .id _ _ := rfl - -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (A B : TopModuleCat.{v} R) (f : A.Hom B) := - f.hom - -initialize_simps_projections Hom (hom' → hom) + hom_type (X →L[R] Y) from (of R X) to (of R Y) variable {R} in /-- Construct an iso in `TopModuleCat` from a continuous linear equiv. -/ diff --git a/Mathlib/Algebra/Category/MonCat/Basic.lean b/Mathlib/Algebra/Category/MonCat/Basic.lean index 70cc261223147a..866c74b8bc0e9e 100644 --- a/Mathlib/Algebra/Category/MonCat/Basic.lean +++ b/Mathlib/Algebra/Category/MonCat/Basic.lean @@ -10,6 +10,7 @@ public import Mathlib.Algebra.Group.TypeTags.Hom public import Mathlib.Algebra.Group.ULift public import Mathlib.CategoryTheory.ConcreteCategory.Forget public import Mathlib.CategoryTheory.Functor.ReflectsIso.Basic +public import Mathlib.Tactic.CategoryTheory.MkConcreteCategory /-! # Category instances for `Monoid`, `AddMonoid`, `CommMonoid`, and `AddCommMonoid`. @@ -63,55 +64,16 @@ abbrev of (M : Type u) [Monoid M] : MonCat := ⟨M⟩ end MonCat -/-- The type of morphisms in `AddMonCat`. -/ -@[ext] -structure AddMonCat.Hom (A B : AddMonCat.{u}) where - private mk :: - /-- The underlying monoid homomorphism. -/ - hom' : A →+ B - -set_option backward.privateInPublic true in -/-- The type of morphisms in `MonCat`. -/ -@[to_additive, ext] -structure MonCat.Hom (A B : MonCat.{u}) where - private mk :: - /-- The underlying monoid homomorphism. -/ - hom' : A →* B +@[to_additive AddMonCat] +mk_concrete_category MonCat.{u} (· →* ·) MonoidHom.id MonoidHom.comp + with_of_hom {X Y : Type u} [Monoid X] [Monoid Y] + hom_type (X →* Y) from (MonCat.of X) to (MonCat.of Y) + to_additive AddMonCat.{u} (· →+ ·) AddMonoidHom.id AddMonoidHom.comp + with_of_hom {X Y : Type u} [AddMonoid X] [AddMonoid Y] + hom_type (X →+ Y) from (AddMonCat.of X) to (AddMonCat.of Y) namespace MonCat -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -@[to_additive] -instance : Category MonCat.{u} where - Hom X Y := Hom X Y - id X := ⟨MonoidHom.id X⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -@[to_additive] -instance : ConcreteCategory MonCat (· →* ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `MonCat` back into a `MonoidHom`. -/ -@[to_additive /-- Turn a morphism in `AddMonCat` back into an `AddMonoidHom`. -/] -abbrev Hom.hom {X Y : MonCat.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := MonCat) f - -/-- Typecheck a `MonoidHom` as a morphism in `MonCat`. -/ -@[to_additive /-- Typecheck an `AddMonoidHom` as a morphism in `AddMonCat`. -/] -abbrev ofHom {X Y : Type u} [Monoid X] [Monoid Y] (f : X →* Y) : of X ⟶ of Y := - ConcreteCategory.ofHom (C := MonCat) f - -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : MonCat.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) -initialize_simps_projections AddMonCat.Hom (hom' → hom) - /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ @@ -134,18 +96,11 @@ lemma ext {X Y : MonCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := -- This is not `simp` to avoid rewriting in types of terms. theorem coe_of (M : Type u) [Monoid M] : (MonCat.of M : Type u) = M := rfl -@[to_additive (attr := simp)] -lemma hom_id {M : MonCat} : (𝟙 M : M ⟶ M).hom = MonoidHom.id M := rfl - /- Provided for rewriting. -/ @[to_additive] lemma id_apply (M : MonCat) (x : M) : (𝟙 M : M ⟶ M) x = x := by simp -@[to_additive (attr := simp)] -lemma hom_comp {M N T : MonCat} (f : M ⟶ N) (g : N ⟶ T) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ @[to_additive] lemma comp_apply {M N T : MonCat} (f : M ⟶ N) (g : N ⟶ T) (x : M) : @@ -155,13 +110,6 @@ lemma comp_apply {M N T : MonCat} (f : M ⟶ N) (g : N ⟶ T) (x : M) : lemma hom_ext {M N : MonCat} {f g : M ⟶ N} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[to_additive (attr := simp)] -lemma hom_ofHom {M N : Type u} [Monoid M] [Monoid N] (f : M →* N) : (ofHom f).hom = f := rfl - -@[to_additive (attr := simp)] -lemma ofHom_hom {M N : MonCat} (f : M ⟶ N) : - ofHom (Hom.hom f) = f := rfl - @[to_additive (attr := simp)] lemma ofHom_id {M : Type u} [Monoid M] : ofHom (MonoidHom.id M) = 𝟙 (of M) := rfl @@ -249,56 +197,16 @@ abbrev of (M : Type u) [CommMonoid M] : CommMonCat := ⟨M⟩ end CommMonCat -/-- The type of morphisms in `AddCommMonCat`. -/ -@[ext] -structure AddCommMonCat.Hom (A B : AddCommMonCat.{u}) where - private mk :: - /-- The underlying monoid homomorphism. -/ - hom' : A →+ B - -set_option backward.privateInPublic true in -/-- The type of morphisms in `CommMonCat`. -/ -@[to_additive, ext] -structure CommMonCat.Hom (A B : CommMonCat.{u}) where - private mk :: - /-- The underlying monoid homomorphism. -/ - hom' : A →* B +@[to_additive AddCommMonCat] +mk_concrete_category CommMonCat.{u} (· →* ·) MonoidHom.id MonoidHom.comp + with_of_hom {X Y : Type u} [CommMonoid X] [CommMonoid Y] + hom_type (X →* Y) from (CommMonCat.of X) to (CommMonCat.of Y) + to_additive AddCommMonCat.{u} (· →+ ·) AddMonoidHom.id AddMonoidHom.comp + with_of_hom {X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] + hom_type (X →+ Y) from (AddCommMonCat.of X) to (AddCommMonCat.of Y) namespace CommMonCat -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -@[to_additive] -instance : Category CommMonCat.{u} where - Hom X Y := Hom X Y - id X := ⟨MonoidHom.id X⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -@[to_additive] -instance : ConcreteCategory CommMonCat (· →* ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `CommMonCat` back into a `MonoidHom`. -/ -@[to_additive /-- Turn a morphism in `AddCommMonCat` back into an `AddMonoidHom`. -/] -abbrev Hom.hom {X Y : CommMonCat.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := CommMonCat) f - -/-- Typecheck a `MonoidHom` as a morphism in `CommMonCat`. -/ -@[to_additive /-- Typecheck an `AddMonoidHom` as a morphism in `AddCommMonCat`. -/] -abbrev ofHom {X Y : Type u} [CommMonoid X] [CommMonoid Y] (f : X →* Y) : of X ⟶ of Y := - ConcreteCategory.ofHom (C := CommMonCat) f - -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -@[to_additive /-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/] -def Hom.Simps.hom (X Y : CommMonCat.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) -initialize_simps_projections AddCommMonCat.Hom (hom' → hom) - /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ @@ -315,18 +223,11 @@ lemma coe_comp {X Y Z : CommMonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X lemma ext {X Y : CommMonCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := ConcreteCategory.hom_ext _ _ w -@[to_additive (attr := simp)] -lemma hom_id {M : CommMonCat} : (𝟙 M : M ⟶ M).hom = MonoidHom.id M := rfl - /- Provided for rewriting. -/ @[to_additive] lemma id_apply (M : CommMonCat) (x : M) : (𝟙 M : M ⟶ M) x = x := by simp -@[to_additive (attr := simp)] -lemma hom_comp {M N T : CommMonCat} (f : M ⟶ N) (g : N ⟶ T) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ @[to_additive] lemma comp_apply {M N T : CommMonCat} (f : M ⟶ N) (g : N ⟶ T) (x : M) : @@ -336,13 +237,6 @@ lemma comp_apply {M N T : CommMonCat} (f : M ⟶ N) (g : N ⟶ T) (x : M) : lemma hom_ext {M N : CommMonCat} {f g : M ⟶ N} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[to_additive (attr := simp)] -lemma hom_ofHom {M N : Type u} [CommMonoid M] [CommMonoid N] (f : M →* N) : (ofHom f).hom = f := rfl - -@[to_additive (attr := simp)] -lemma ofHom_hom {M N : CommMonCat} (f : M ⟶ N) : - ofHom (Hom.hom f) = f := rfl - @[to_additive (attr := simp)] lemma ofHom_id {M : Type u} [CommMonoid M] : ofHom (MonoidHom.id M) = 𝟙 (of M) := rfl diff --git a/Mathlib/Algebra/Category/Ring/Basic.lean b/Mathlib/Algebra/Category/Ring/Basic.lean index 026c44a5d74c06..89b6bc47050653 100644 --- a/Mathlib/Algebra/Category/Ring/Basic.lean +++ b/Mathlib/Algebra/Category/Ring/Basic.lean @@ -63,57 +63,18 @@ lemma coe_of (R : Type u) [Semiring R] : (of R : Type u) = R := lemma of_carrier (R : SemiRingCat.{u}) : of R = R := rfl -set_option backward.privateInPublic true in -variable {R} in -/-- The type of morphisms in `SemiRingCat`. -/ -@[ext] -structure Hom (R S : SemiRingCat.{u}) where - private mk :: - /-- The underlying ring hom. -/ - hom' : R →+* S - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category SemiRingCat where - Hom R S := Hom R S - id R := ⟨RingHom.id R⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory.{u} SemiRingCat (fun R S => R →+* S) where - hom := Hom.hom' - ofHom f := ⟨f⟩ - -/-- Turn a morphism in `SemiRingCat` back into a `RingHom`. -/ -abbrev Hom.hom {R S : SemiRingCat.{u}} (f : Hom R S) := - ConcreteCategory.hom (C := SemiRingCat) f - -/-- Typecheck a `RingHom` as a morphism in `SemiRingCat`. -/ -abbrev ofHom {R S : Type u} [Semiring R] [Semiring S] (f : R →+* S) : of R ⟶ of S := - ConcreteCategory.ofHom (C := SemiRingCat) f - -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (R S : SemiRingCat) (f : Hom R S) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category SemiRingCat.{u} (· →+* ·) RingHom.id RingHom.comp + with_of_hom {R S : Type u} [Semiring R] [Semiring S] + hom_type (R →+* S) from (SemiRingCat.of R) to (SemiRingCat.of S) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ -@[simp] -lemma hom_id {R : SemiRingCat} : (𝟙 R : R ⟶ R).hom = RingHom.id R := rfl - /- Provided for rewriting. -/ lemma id_apply (R : SemiRingCat) (r : R) : (𝟙 R : R ⟶ R) r = r := by simp -@[simp] -lemma hom_comp {R S T : SemiRingCat} (f : R ⟶ S) (g : S ⟶ T) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {R S T : SemiRingCat} (f : R ⟶ S) (g : S ⟶ T) (r : R) : (f ≫ g) r = g (f r) := by simp @@ -122,13 +83,6 @@ lemma comp_apply {R S T : SemiRingCat} (f : R ⟶ S) (g : S ⟶ T) (r : R) : lemma hom_ext {R S : SemiRingCat} {f g : R ⟶ S} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {R S : Type u} [Semiring R] [Semiring S] (f : R →+* S) : (ofHom f).hom = f := rfl - -@[simp] -lemma ofHom_hom {R S : SemiRingCat} (f : R ⟶ S) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {R : Type u} [Semiring R] : ofHom (RingHom.id R) = 𝟙 (of R) := rfl @@ -229,57 +183,18 @@ lemma coe_of (R : Type u) [Ring R] : (of R : Type u) = R := lemma of_carrier (R : RingCat.{u}) : of R = R := rfl -set_option backward.privateInPublic true in -variable {R} in -/-- The type of morphisms in `RingCat`. -/ -@[ext] -structure Hom (R S : RingCat.{u}) where - private mk :: - /-- The underlying ring hom. -/ - hom' : R →+* S - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category RingCat where - Hom R S := Hom R S - id R := ⟨RingHom.id R⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory.{u} RingCat (fun R S => R →+* S) where - hom := Hom.hom' - ofHom f := ⟨f⟩ - -/-- Turn a morphism in `RingCat` back into a `RingHom`. -/ -abbrev Hom.hom {R S : RingCat.{u}} (f : Hom R S) := - ConcreteCategory.hom (C := RingCat) f - -/-- Typecheck a `RingHom` as a morphism in `RingCat`. -/ -abbrev ofHom {R S : Type u} [Ring R] [Ring S] (f : R →+* S) : of R ⟶ of S := - ConcreteCategory.ofHom (C := RingCat) f - -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (R S : RingCat) (f : Hom R S) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category RingCat.{u} (· →+* ·) RingHom.id RingHom.comp + with_of_hom {R S : Type u} [Ring R] [Ring S] + hom_type (R →+* S) from (RingCat.of R) to (RingCat.of S) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ -@[simp] -lemma hom_id {R : RingCat} : (𝟙 R : R ⟶ R).hom = RingHom.id R := rfl - /- Provided for rewriting. -/ lemma id_apply (R : RingCat) (r : R) : (𝟙 R : R ⟶ R) r = r := by simp -@[simp] -lemma hom_comp {R S T : RingCat} (f : R ⟶ S) (g : S ⟶ T) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {R S T : RingCat} (f : R ⟶ S) (g : S ⟶ T) (r : R) : (f ≫ g) r = g (f r) := by simp @@ -288,13 +203,6 @@ lemma comp_apply {R S T : RingCat} (f : R ⟶ S) (g : S ⟶ T) (r : R) : lemma hom_ext {R S : RingCat} {f g : R ⟶ S} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {R S : Type u} [Ring R] [Ring S] (f : R →+* S) : (ofHom f).hom = f := rfl - -@[simp] -lemma ofHom_hom {R S : RingCat} (f : R ⟶ S) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {R : Type u} [Ring R] : ofHom (RingHom.id R) = 𝟙 (of R) := rfl @@ -404,57 +312,18 @@ lemma coe_of (R : Type u) [CommSemiring R] : (of R : Type u) = R := lemma of_carrier (R : CommSemiRingCat.{u}) : of R = R := rfl -set_option backward.privateInPublic true in -variable {R} in -/-- The type of morphisms in `CommSemiRingCat`. -/ -@[ext] -structure Hom (R S : CommSemiRingCat.{u}) where - private mk :: - /-- The underlying ring hom. -/ - hom' : R →+* S - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category CommSemiRingCat where - Hom R S := Hom R S - id R := ⟨RingHom.id R⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory.{u} CommSemiRingCat (fun R S => R →+* S) where - hom := Hom.hom' - ofHom f := ⟨f⟩ - -/-- Turn a morphism in `CommSemiRingCat` back into a `RingHom`. -/ -abbrev Hom.hom {R S : CommSemiRingCat.{u}} (f : Hom R S) := - ConcreteCategory.hom (C := CommSemiRingCat) f - -/-- Typecheck a `RingHom` as a morphism in `CommSemiRingCat`. -/ -abbrev ofHom {R S : Type u} [CommSemiring R] [CommSemiring S] (f : R →+* S) : of R ⟶ of S := - ConcreteCategory.ofHom (C := CommSemiRingCat) f - -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (R S : CommSemiRingCat) (f : Hom R S) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category CommSemiRingCat.{u} (· →+* ·) RingHom.id RingHom.comp + with_of_hom {R S : Type u} [CommSemiring R] [CommSemiring S] + hom_type (R →+* S) from (CommSemiRingCat.of R) to (CommSemiRingCat.of S) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ -@[simp] -lemma hom_id {R : CommSemiRingCat} : (𝟙 R : R ⟶ R).hom = RingHom.id R := rfl - /- Provided for rewriting. -/ lemma id_apply (R : CommSemiRingCat) (r : R) : (𝟙 R : R ⟶ R) r = r := by simp -@[simp] -lemma hom_comp {R S T : CommSemiRingCat} (f : R ⟶ S) (g : S ⟶ T) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {R S T : CommSemiRingCat} (f : R ⟶ S) (g : S ⟶ T) (r : R) : (f ≫ g) r = g (f r) := by simp @@ -463,14 +332,6 @@ lemma comp_apply {R S T : CommSemiRingCat} (f : R ⟶ S) (g : S ⟶ T) (r : R) : lemma hom_ext {R S : CommSemiRingCat} {f g : R ⟶ S} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {R S : Type u} [CommSemiring R] [CommSemiring S] (f : R →+* S) : - (ofHom f).hom = f := rfl - -@[simp] -lemma ofHom_hom {R S : CommSemiRingCat} (f : R ⟶ S) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {R : Type u} [CommSemiring R] : ofHom (RingHom.id R) = 𝟙 (of R) := rfl @@ -577,57 +438,18 @@ lemma coe_of (R : Type u) [CommRing R] : (of R : Type u) = R := lemma of_carrier (R : CommRingCat.{u}) : of R = R := rfl -set_option backward.privateInPublic true in -variable {R} in -/-- The type of morphisms in `CommRingCat`. -/ -@[ext] -structure Hom (R S : CommRingCat.{u}) where - private mk :: - /-- The underlying ring hom. -/ - hom' : R →+* S - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category CommRingCat where - Hom R S := Hom R S - id R := ⟨RingHom.id R⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory.{u} CommRingCat (fun R S => R →+* S) where - hom := Hom.hom' - ofHom f := ⟨f⟩ - -/-- The underlying ring hom. -/ -abbrev Hom.hom {R S : CommRingCat.{u}} (f : Hom R S) := - ConcreteCategory.hom (C := CommRingCat) f - -/-- Typecheck a `RingHom` as a morphism in `CommRingCat`. -/ -abbrev ofHom {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : of R ⟶ of S := - ConcreteCategory.ofHom (C := CommRingCat) f - -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (R S : CommRingCat) (f : Hom R S) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category CommRingCat.{u} (· →+* ·) RingHom.id RingHom.comp + with_of_hom {R S : Type u} [CommRing R] [CommRing S] + hom_type (R →+* S) from (CommRingCat.of R) to (CommRingCat.of S) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ -@[simp] -lemma hom_id {R : CommRingCat} : (𝟙 R : R ⟶ R).hom = RingHom.id R := rfl - /- Provided for rewriting. -/ lemma id_apply (R : CommRingCat) (r : R) : (𝟙 R : R ⟶ R) r = r := by simp -@[simp] -lemma hom_comp {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) (r : R) : (f ≫ g) r = g (f r) := by simp @@ -636,13 +458,6 @@ lemma comp_apply {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) (r : R) : lemma hom_ext {R S : CommRingCat} {f g : R ⟶ S} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : (ofHom f).hom = f := rfl - -@[simp] -lemma ofHom_hom {R S : CommRingCat} (f : R ⟶ S) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {R : Type u} [CommRing R] : ofHom (RingHom.id R) = 𝟙 (of R) := rfl diff --git a/Mathlib/Algebra/Category/Semigrp/Basic.lean b/Mathlib/Algebra/Category/Semigrp/Basic.lean index 6e146186a8c4a1..555db57c36ccdc 100644 --- a/Mathlib/Algebra/Category/Semigrp/Basic.lean +++ b/Mathlib/Algebra/Category/Semigrp/Basic.lean @@ -9,6 +9,7 @@ public import Mathlib.Algebra.PEmptyInstances public import Mathlib.Algebra.Group.Equiv.Defs public import Mathlib.CategoryTheory.ConcreteCategory.Forget public import Mathlib.CategoryTheory.Functor.ReflectsIso.Basic +public import Mathlib.Tactic.CategoryTheory.MkConcreteCategory /-! # Category instances for `Mul`, `Add`, `Semigroup` and `AddSemigroup` @@ -68,56 +69,16 @@ abbrev of (M : Type u) [Mul M] : MagmaCat := ⟨M⟩ end MagmaCat -/-- The type of morphisms in `AddMagmaCat R`. -/ -@[ext] -structure AddMagmaCat.Hom (A B : AddMagmaCat.{u}) where - private mk :: - /-- The underlying `AddHom`. -/ - hom' : A →ₙ+ B - -set_option backward.privateInPublic true in -/-- The type of morphisms in `MagmaCat R`. -/ -@[to_additive, ext] -structure MagmaCat.Hom (A B : MagmaCat.{u}) where - private mk :: - /-- The underlying `MulHom`. -/ - hom' : A →ₙ* B +@[to_additive AddMagmaCat] +mk_concrete_category MagmaCat.{u} (· →ₙ* ·) MulHom.id MulHom.comp + with_of_hom {X Y : Type u} [Mul X] [Mul Y] + hom_type (X →ₙ* Y) from (MagmaCat.of X) to (MagmaCat.of Y) + to_additive AddMagmaCat.{u} (· →ₙ+ ·) AddHom.id AddHom.comp + with_of_hom {X Y : Type u} [Add X] [Add Y] + hom_type (X →ₙ+ Y) from (AddMagmaCat.of X) to (AddMagmaCat.of Y) namespace MagmaCat -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -@[to_additive] -instance : Category MagmaCat.{u} where - Hom X Y := Hom X Y - id X := ⟨MulHom.id X⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -@[to_additive] -instance : ConcreteCategory MagmaCat (· →ₙ* ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `MagmaCat` back into a `MulHom`. -/ -@[to_additive /-- Turn a morphism in `AddMagmaCat` back into an `AddHom`. -/] -abbrev Hom.hom {X Y : MagmaCat.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := MagmaCat) f - -/-- Typecheck a `MulHom` as a morphism in `MagmaCat`. -/ -@[to_additive /-- Typecheck an `AddHom` as a morphism in `AddMagmaCat`. -/] -abbrev ofHom {X Y : Type u} [Mul X] [Mul Y] (f : X →ₙ* Y) : of X ⟶ of Y := - ConcreteCategory.ofHom (C := MagmaCat) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : MagmaCat.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) -initialize_simps_projections AddMagmaCat.Hom (hom' → hom) - /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ @@ -138,18 +99,11 @@ lemma ext {X Y : MagmaCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := -- This is not `simp` to avoid rewriting in types of terms. theorem coe_of (M : Type u) [Mul M] : (MagmaCat.of M : Type u) = M := rfl -@[to_additive (attr := simp)] -lemma hom_id {M : MagmaCat} : (𝟙 M : M ⟶ M).hom = MulHom.id M := rfl - /- Provided for rewriting. -/ @[to_additive] lemma id_apply (M : MagmaCat) (x : M) : (𝟙 M : M ⟶ M) x = x := by simp -@[to_additive (attr := simp)] -lemma hom_comp {M N T : MagmaCat} (f : M ⟶ N) (g : N ⟶ T) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ @[to_additive] lemma comp_apply {M N T : MagmaCat} (f : M ⟶ N) (g : N ⟶ T) (x : M) : @@ -159,13 +113,6 @@ lemma comp_apply {M N T : MagmaCat} (f : M ⟶ N) (g : N ⟶ T) (x : M) : lemma hom_ext {M N : MagmaCat} {f g : M ⟶ N} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[to_additive (attr := simp)] -lemma hom_ofHom {M N : Type u} [Mul M] [Mul N] (f : M →ₙ* N) : (ofHom f).hom = f := rfl - -@[to_additive (attr := simp)] -lemma ofHom_hom {M N : MagmaCat} (f : M ⟶ N) : - ofHom (Hom.hom f) = f := rfl - @[to_additive (attr := simp)] lemma ofHom_id {M : Type u} [Mul M] : ofHom (MulHom.id M) = 𝟙 (of M) := rfl @@ -230,56 +177,16 @@ abbrev of (M : Type u) [Semigroup M] : Semigrp := ⟨M⟩ end Semigrp -/-- The type of morphisms in `AddSemigrp R`. -/ -@[ext] -structure AddSemigrp.Hom (A B : AddSemigrp.{u}) where - private mk :: - /-- The underlying `AddHom`. -/ - hom' : A →ₙ+ B - -set_option backward.privateInPublic true in -/-- The type of morphisms in `Semigrp R`. -/ -@[to_additive, ext] -structure Semigrp.Hom (A B : Semigrp.{u}) where - private mk :: - /-- The underlying `MulHom`. -/ - hom' : A →ₙ* B +@[to_additive AddSemigrp] +mk_concrete_category Semigrp.{u} (· →ₙ* ·) MulHom.id MulHom.comp + with_of_hom {X Y : Type u} [Semigroup X] [Semigroup Y] + hom_type (X →ₙ* Y) from (Semigrp.of X) to (Semigrp.of Y) + to_additive AddSemigrp.{u} (· →ₙ+ ·) AddHom.id AddHom.comp + with_of_hom {X Y : Type u} [AddSemigroup X] [AddSemigroup Y] + hom_type (X →ₙ+ Y) from (AddSemigrp.of X) to (AddSemigrp.of Y) namespace Semigrp -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -@[to_additive] -instance : Category Semigrp.{u} where - Hom X Y := Hom X Y - id X := ⟨MulHom.id X⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -@[to_additive] -instance : ConcreteCategory Semigrp (· →ₙ* ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `Semigrp` back into a `MulHom`. -/ -@[to_additive /-- Turn a morphism in `AddSemigrp` back into an `AddHom`. -/] -abbrev Hom.hom {X Y : Semigrp.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := Semigrp) f - -/-- Typecheck a `MulHom` as a morphism in `Semigrp`. -/ -@[to_additive /-- Typecheck an `AddHom` as a morphism in `AddSemigrp`. -/] -abbrev ofHom {X Y : Type u} [Semigroup X] [Semigroup Y] (f : X →ₙ* Y) : of X ⟶ of Y := - ConcreteCategory.ofHom (C := Semigrp) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : Semigrp.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) -initialize_simps_projections AddSemigrp.Hom (hom' → hom) - /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ @@ -301,18 +208,11 @@ lemma ext {X Y : Semigrp} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := theorem coe_of (R : Type u) [Semigroup R] : ↑(Semigrp.of R) = R := rfl -@[to_additive (attr := simp)] -lemma hom_id {X : Semigrp} : (𝟙 X : X ⟶ X).hom = MulHom.id X := rfl - /- Provided for rewriting. -/ @[to_additive] lemma id_apply (X : Semigrp) (x : X) : (𝟙 X : X ⟶ X) x = x := by simp -@[to_additive (attr := simp)] -lemma hom_comp {X Y T : Semigrp} (f : X ⟶ Y) (g : Y ⟶ T) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ @[to_additive] lemma comp_apply {X Y T : Semigrp} (f : X ⟶ Y) (g : Y ⟶ T) (x : X) : @@ -322,13 +222,6 @@ lemma comp_apply {X Y T : Semigrp} (f : X ⟶ Y) (g : Y ⟶ T) (x : X) : lemma hom_ext {X Y : Semigrp} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[to_additive (attr := simp)] -lemma hom_ofHom {X Y : Type u} [Semigroup X] [Semigroup Y] (f : X →ₙ* Y) : (ofHom f).hom = f := rfl - -@[to_additive (attr := simp)] -lemma ofHom_hom {X Y : Semigrp} (f : X ⟶ Y) : - ofHom (Hom.hom f) = f := rfl - @[to_additive (attr := simp)] lemma ofHom_id {X : Type u} [Semigroup X] : ofHom (MulHom.id X) = 𝟙 (of X) := rfl diff --git a/Mathlib/AlgebraicGeometry/AffineSpace.lean b/Mathlib/AlgebraicGeometry/AffineSpace.lean index b892058edf577c..3540a57b813af9 100644 --- a/Mathlib/AlgebraicGeometry/AffineSpace.lean +++ b/Mathlib/AlgebraicGeometry/AffineSpace.lean @@ -176,9 +176,8 @@ def isoOfIsAffine [IsAffine S] : hom_inv_id := by ext1 · simp only [Category.assoc, homOfVector_over, Category.id_comp] - rw [← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp, eval₂Hom_comp_C, - CommRingCat.ofHom_hom, ← Scheme.toSpecΓ_naturality_assoc] - simp [Scheme.isoSpec] + rw [← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp, eval₂Hom_comp_C] + simp [← Scheme.toSpecΓ_naturality_assoc] · simp inv_hom_id := by apply ext_of_isAffine @@ -299,7 +298,7 @@ lemma map_SpecMap {R S : CommRingCat.{max u v}} (φ : R ⟶ S) : ext1 · simp only [map_over, Category.assoc, SpecIso_inv_over, SpecIso_inv_over_assoc, ← Spec.map_comp, ← CommRingCat.ofHom_comp] - rw [map_comp_C, CommRingCat.ofHom_comp, CommRingCat.ofHom_hom] + simp · simp only [TopologicalSpace.Opens.map_top, Scheme.Hom.comp_app, CommRingCat.comp_apply] conv_lhs => enter [2]; tactic => exact map_appTop_coord _ _ conv_rhs => enter [2]; tactic => exact SpecIso_inv_appTop_coord _ _ diff --git a/Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean b/Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean index 339afd4cfd4147..225cd0af275030 100644 --- a/Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean +++ b/Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean @@ -146,7 +146,8 @@ lemma glueDataObjMap_glueDataObjι {U V : X.affineOpens} (h : U ≤ V) : Ideal.quotientMap_comp_mk, CommRingCat.ofHom_comp, Spec.map_comp_assoc, glueDataObjι, Category.assoc] congr 1 - rw [Iso.eq_inv_comp, IsAffineOpen.isoSpec_hom, CommRingCat.ofHom_hom] + rw [Iso.eq_inv_comp, IsAffineOpen.isoSpec_hom] + dsimp erw [Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc U.1 V.1 h] rw [← IsAffineOpen.isoSpec_hom V.2, Iso.hom_inv_id, Category.comp_id] @@ -725,7 +726,7 @@ lemma Hom.toImage_app : ← IsIso.eq_comp_inv, ← Functor.map_inv] simp only [Hom.comp_base, Opens.map_comp_obj, Category.assoc, Iso.inv_hom_id_assoc, eqToHom_op, inv_eqToHom] - rw [← reassoc_of% CommRingCat.ofHom_comp, Ideal.Quotient.lift_comp_mk, CommRingCat.ofHom_hom, + rw [← reassoc_of% CommRingCat.ofHom_comp, Ideal.Quotient.lift_comp_mk, eqToHom_refl, CategoryTheory.Functor.map_id] exact (Category.comp_id _).symm diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean b/Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean index b3f98d4d043570..47cb50bbb7a6c0 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean @@ -216,8 +216,9 @@ instance smoothOfRelativeDimension_comp {Z : Scheme.{u}} (g : Y ⟶ Z) have heq : (f ≫ g).appLE U₂ (X.basicOpen s) e = g.appLE U₂ V₂ e₂ ≫ CommRingCat.ofHom (algebraMap Γ(Y, V₂) Γ(Y, Y.basicOpen r)) ≫ f.appLE (Y.basicOpen r) (X.basicOpen s) e₁ := by - rw [RingHom.algebraMap_toAlgebra, CommRingCat.ofHom_hom, - g.appLE_map_assoc, Scheme.Hom.appLE_comp_appLE] + rw [RingHom.algebraMap_toAlgebra] + dsimp + rw [g.appLE_map_assoc, Scheme.Hom.appLE_comp_appLE] refine ⟨U₂, hU₂, X.basicOpen s, hV₁'.basicOpen s, hx₁, e, heq ▸ ?_⟩ apply IsStandardSmoothOfRelativeDimension.comp ?_ hf₂ haveI : IsLocalization.Away r Γ(Y, Y.basicOpen r) := hV₂.isLocalization_basicOpen r diff --git a/Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean b/Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean index 9340a9f55f8c3a..63622951ad3c52 100644 --- a/Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean +++ b/Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean @@ -9,6 +9,7 @@ public import Mathlib.Analysis.Normed.Group.Constructions public import Mathlib.Analysis.Normed.Group.Hom public import Mathlib.CategoryTheory.ConcreteCategory.Forget public import Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms +public import Mathlib.Tactic.CategoryTheory.MkConcreteCategory /-! # The category of seminormed groups @@ -41,35 +42,10 @@ namespace SemiNormedGrp instance : CoeSort SemiNormedGrp Type* where coe X := X.carrier -/-- The type of morphisms in `SemiNormedGrp` -/ -@[ext] -structure Hom (M N : SemiNormedGrp.{u}) where - /-- The underlying `NormedAddGroupHom`. -/ - hom' : NormedAddGroupHom M N - -instance : LargeCategory.{u} SemiNormedGrp where - Hom X Y := Hom X Y - id X := ⟨NormedAddGroupHom.id X⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -instance : ConcreteCategory SemiNormedGrp (NormedAddGroupHom · ·) where - hom f := f.hom' - ofHom f := ⟨f⟩ - -/-- Turn a morphism in `SemiNormedGrp` back into a `NormedAddGroupHom`. -/ -abbrev Hom.hom {M N : SemiNormedGrp.{u}} (f : Hom M N) := - ConcreteCategory.hom (C := SemiNormedGrp) f - -/-- Typecheck a `NormedAddGroupHom` as a morphism in `SemiNormedGrp`. -/ -abbrev ofHom {M N : Type u} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] - (f : NormedAddGroupHom M N) : of M ⟶ of N := - ConcreteCategory.ofHom (C := SemiNormedGrp) f - -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (M N : SemiNormedGrp.{u}) (f : Hom M N) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category SemiNormedGrp.{u} (NormedAddGroupHom · ·) + NormedAddGroupHom.id NormedAddGroupHom.comp + with_of_hom {M N : Type u} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] + hom_type (NormedAddGroupHom M N) from (of M) to (of N) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. @@ -78,17 +54,10 @@ The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep lemma ext {M N : SemiNormedGrp} {f₁ f₂ : M ⟶ N} (h : ∀ (x : M), f₁ x = f₂ x) : f₁ = f₂ := ConcreteCategory.ext_apply h -@[simp] -lemma hom_id {M : SemiNormedGrp} : (𝟙 M : M ⟶ M).hom = NormedAddGroupHom.id M := rfl - /- Provided for rewriting. -/ lemma id_apply (M : SemiNormedGrp) (r : M) : (𝟙 M : M ⟶ M) r = r := by simp -@[simp] -lemma hom_comp {M N O : SemiNormedGrp} (f : M ⟶ N) (g : N ⟶ O) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {M N O : SemiNormedGrp} (f : M ⟶ N) (g : N ⟶ O) (r : M) : (f ≫ g) r = g (f r) := by simp @@ -97,14 +66,6 @@ lemma comp_apply {M N O : SemiNormedGrp} (f : M ⟶ N) (g : N ⟶ O) (r : M) : lemma hom_ext {M N : SemiNormedGrp} {f g : M ⟶ N} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {M N : Type u} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] - (f : NormedAddGroupHom M N) : (ofHom f).hom = f := rfl - -@[simp] -lemma ofHom_hom {M N : SemiNormedGrp} (f : M ⟶ N) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {M : Type u} [SeminormedAddCommGroup M] : ofHom (NormedAddGroupHom.id M) = 𝟙 (of M) := rfl diff --git a/Mathlib/Condensed/Light/Sequence.lean b/Mathlib/Condensed/Light/Sequence.lean index 541eb9ab95c7af..55e559602dd8c3 100644 --- a/Mathlib/Condensed/Light/Sequence.lean +++ b/Mathlib/Condensed/Light/Sequence.lean @@ -32,7 +32,7 @@ def LightProfinite.fibre : LightProfinite := isCompact_iff_compactSpace.mp (IsClosed.preimage (by fun_prop) isClosed_singleton).isCompact of (f ⁻¹' {y}) -def LightProfinite.fibreIncl : fibre y f ⟶ X := ⟨⟨{ toFun := Subtype.val }⟩⟩ +def LightProfinite.fibreIncl : fibre y f ⟶ X := ⟨TopCat.ofHom { toFun := Subtype.val }⟩ end @@ -190,9 +190,9 @@ are equal. This can be checked by precomposing with an epimorphism, which is given by this morphism. -/ def cover {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) : (of _ (T ⊕ (pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) - (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)))) ⟶ pullback π π := ⟨⟨{ + (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)))) ⟶ pullback π π := ⟨TopCat.ofHom { toFun := coverToFun _ _ - continuous_toFun := by dsimp [coverToFun]; fun_prop }⟩⟩ + continuous_toFun := by dsimp [coverToFun]; fun_prop }⟩ open Limits in set_option backward.isDefEq.respectTransparency false in @@ -262,7 +262,7 @@ lemma aux {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π] : -- `fibres`. have := S'_compactSpace π (by fun_prop) let S'π (n : ℕ∪{∞}) : LightProfinite.of (S' π) ⟶ LightProfinite.fibre n (π ≫ snd _ _) := - ⟨⟨{ toFun x := x.val n, continuous_toFun := by refine (continuous_apply _).comp ?_; fun_prop }⟩⟩ + ⟨TopCat.ofHom ⟨fun x ↦ x.val n, by refine (continuous_apply _).comp ?_; fun_prop⟩⟩ let y' : LightProfinite.of (S' π) ⟶ S := ConcreteCategory.ofHom ⟨y π, y_continuous π⟩ let π' := pullback.snd π (y' ▷ ℕ∪{∞}) let σ' : ℕ∪{∞} → LightProfinite.of (S' π) → pullback π (y' ▷ ℕ∪{∞}) := fun n ↦ @@ -276,8 +276,8 @@ lemma aux {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π] : have : CompactSpace (fibres π' σ') := isCompact_iff_compactSpace.mp (fibres_closed π' (by fun_prop) σ' (by fun_prop) hσ').isCompact refine ⟨LightProfinite.of (S' π), LightProfinite.of (fibres π' σ'), y', - ⟨⟨Subtype.val, by fun_prop⟩⟩ ≫ π', - ⟨⟨Subtype.val, by fun_prop⟩⟩ ≫ pullback.fst _ _, ?_, ?_, ?_, ?_, ?_⟩ + ⟨TopCat.ofHom ⟨Subtype.val, by fun_prop⟩⟩ ≫ π', + ⟨TopCat.ofHom ⟨Subtype.val, by fun_prop⟩⟩ ≫ pullback.fst _ _, ?_, ?_, ?_, ?_, ?_⟩ · rw [LightProfinite.epi_iff_surjective] refine fibres_surjective _ ?_ _ hσ hσ' rw [← LightProfinite.epi_iff_surjective] diff --git a/Mathlib/Order/Category/BddDistLat.lean b/Mathlib/Order/Category/BddDistLat.lean index f8d8b199964fdf..eb3c8bb09f2406 100644 --- a/Mathlib/Order/Category/BddDistLat.lean +++ b/Mathlib/Order/Category/BddDistLat.lean @@ -48,43 +48,11 @@ abbrev of (α : Type*) [DistribLattice α] [BoundedOrder α] : BddDistLat where theorem coe_of (α : Type*) [DistribLattice α] [BoundedOrder α] : ↥(of α) = α := rfl -set_option backward.privateInPublic true in -/-- The type of morphisms in `BddDistLat R`. -/ -@[ext] -structure Hom (X Y : BddDistLat.{u}) where - private mk :: - /-- The underlying `BoundedLatticeHom`. -/ - hom' : BoundedLatticeHom X Y - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category BddDistLat.{u} where - Hom X Y := Hom X Y - id X := ⟨BoundedLatticeHom.id X⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory BddDistLat (BoundedLatticeHom · ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `BddDistLat` back into a `BoundedLatticeHom`. -/ -abbrev Hom.hom {X Y : BddDistLat.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := BddDistLat) f - -/-- Typecheck a `BoundedLatticeHom` as a morphism in `BddDistLat`. -/ -abbrev ofHom {X Y : Type u} [DistribLattice X] [BoundedOrder X] [DistribLattice Y] [BoundedOrder Y] - (f : BoundedLatticeHom X Y) : - of X ⟶ of Y := - ConcreteCategory.ofHom (C := BddDistLat) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : BddDistLat.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category BddDistLat.{u} (BoundedLatticeHom · ·) + (fun (X : BddDistLat) ↦ BoundedLatticeHom.id X) + BoundedLatticeHom.comp + with_of_hom {X Y : Type u} [DistribLattice X] [BoundedOrder X] [DistribLattice Y] + [BoundedOrder Y] hom_type (BoundedLatticeHom X Y) from (of X) to (of Y) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. @@ -104,17 +72,10 @@ lemma forget_map {X Y : BddDistLat} (f : X ⟶ Y) : lemma ext {X Y : BddDistLat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := ConcreteCategory.hom_ext _ _ w -@[simp] -lemma hom_id {X : BddDistLat} : (𝟙 X : X ⟶ X).hom = BoundedLatticeHom.id _ := rfl - /- Provided for rewriting. -/ lemma id_apply (X : BddDistLat) (x : X) : (𝟙 X : X ⟶ X) x = x := by simp -@[simp] -lemma hom_comp {X Y Z : BddDistLat} (f : X ⟶ Y) (g : Y ⟶ Z) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {X Y Z : BddDistLat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp @@ -123,16 +84,6 @@ lemma comp_apply {X Y Z : BddDistLat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : lemma hom_ext {X Y : BddDistLat} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {X Y : Type u} [DistribLattice X] [BoundedOrder X] [DistribLattice Y] - [BoundedOrder Y] (f : BoundedLatticeHom X Y) : - (ofHom f).hom = f := - rfl - -@[simp] -lemma ofHom_hom {X Y : BddDistLat} (f : X ⟶ Y) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {X : Type u} [DistribLattice X] [BoundedOrder X] : ofHom (BoundedLatticeHom.id _) = 𝟙 (of X) := rfl diff --git a/Mathlib/Order/Category/BddLat.lean b/Mathlib/Order/Category/BddLat.lean index 508c5f4f137be2..99a6aa2fee422f 100644 --- a/Mathlib/Order/Category/BddLat.lean +++ b/Mathlib/Order/Category/BddLat.lean @@ -48,57 +48,18 @@ abbrev of (α : Type*) [Lattice α] [BoundedOrder α] : BddLat where theorem coe_of (α : Type*) [Lattice α] [BoundedOrder α] : ↥(of α) = α := rfl -set_option backward.privateInPublic true in -/-- The type of morphisms in `BddLat`. -/ -@[ext] -structure Hom (X Y : BddLat.{u}) where - private mk :: - /-- The underlying `BoundedLatticeHom`. -/ - hom' : BoundedLatticeHom X Y - instance : Inhabited BddLat := ⟨of PUnit⟩ -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : LargeCategory.{u} BddLat where - Hom := Hom - id X := ⟨BoundedLatticeHom.id X⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory BddLat (BoundedLatticeHom · ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `BddLat` back into a `BoundedLatticeHom`. -/ -abbrev Hom.hom {X Y : BddLat.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := BddLat) f - -/-- Typecheck a `BoundedLatticeHom` as a morphism in `BddLat`. -/ -abbrev ofHom {X Y : Type u} [Lattice X] [BoundedOrder X] [Lattice Y] [BoundedOrder Y] - (f : BoundedLatticeHom X Y) : of X ⟶ of Y := - ConcreteCategory.ofHom (C := BddLat) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : BddLat.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) - -@[simp] -lemma hom_id {X : Lat} : (𝟙 X : X ⟶ X).hom = LatticeHom.id _ := rfl +mk_concrete_category BddLat.{u} (BoundedLatticeHom · ·) (fun (X : BddLat) ↦ BoundedLatticeHom.id X) + BoundedLatticeHom.comp + with_of_hom {X Y : Type u} [Lattice X] [BoundedOrder X] [Lattice Y] [BoundedOrder Y] + hom_type (BoundedLatticeHom X Y) from (of X) to (of Y) /- Provided for rewriting. -/ lemma id_apply (X : Lat) (x : X) : (𝟙 X : X ⟶ X) x = x := by simp -@[simp] -lemma hom_comp {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp diff --git a/Mathlib/Order/Category/BddOrd.lean b/Mathlib/Order/Category/BddOrd.lean index fbda8a11919aec..71669c4dac8c6f 100644 --- a/Mathlib/Order/Category/BddOrd.lean +++ b/Mathlib/Order/Category/BddOrd.lean @@ -42,42 +42,10 @@ instance : CoeSort BddOrd Type* := abbrev of (X : Type*) [PartialOrder X] [BoundedOrder X] : BddOrd where carrier := X -set_option backward.privateInPublic true in -/-- The type of morphisms in `BddOrd R`. -/ -@[ext] -structure Hom (X Y : BddOrd.{u}) where - private mk :: - /-- The underlying `BoundedOrderHom`. -/ - hom' : BoundedOrderHom X Y - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category BddOrd.{u} where - Hom X Y := Hom X Y - id _ := ⟨BoundedOrderHom.id _⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory BddOrd (BoundedOrderHom · ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `BddOrd` back into a `BoundedOrderHom`. -/ -abbrev Hom.hom {X Y : BddOrd.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := BddOrd) f - -/-- Typecheck a `BoundedOrderHom` as a morphism in `BddOrd`. -/ -abbrev ofHom {X Y : Type u} [PartialOrder X] [BoundedOrder X] [PartialOrder Y] [BoundedOrder Y] - (f : BoundedOrderHom X Y) : of X ⟶ of Y := - ConcreteCategory.ofHom (C := BddOrd) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : BddOrd.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category BddOrd.{u} (BoundedOrderHom · ·) (fun (X : BddOrd) ↦ BoundedOrderHom.id X) + BoundedOrderHom.comp + with_of_hom {X Y : Type u} [PartialOrder X] [BoundedOrder X] [PartialOrder Y] + [BoundedOrder Y] hom_type (BoundedOrderHom X Y) from (of X) to (of Y) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. @@ -100,17 +68,10 @@ lemma ext {X Y : BddOrd} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := -- This is not `simp` to avoid rewriting in types of terms. theorem coe_of (X : Type u) [PartialOrder X] [BoundedOrder X] : (BddOrd.of X : Type u) = X := rfl -@[simp] -lemma hom_id {X : BddOrd} : (𝟙 X : X ⟶ X).hom = BoundedOrderHom.id _ := rfl - /- Provided for rewriting. -/ lemma id_apply (X : BddOrd) (x : X) : (𝟙 X : X ⟶ X) x = x := by simp -@[simp] -lemma hom_comp {X Y Z : BddOrd} (f : X ⟶ Y) (g : Y ⟶ Z) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {X Y Z : BddOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp @@ -119,15 +80,6 @@ lemma comp_apply {X Y Z : BddOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : lemma hom_ext {X Y : BddOrd} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {X Y : Type u} [PartialOrder X] [BoundedOrder X] [PartialOrder Y] [BoundedOrder Y] - (f : BoundedOrderHom X Y) : - (ofHom f).hom = f := rfl - -@[simp] -lemma ofHom_hom {X Y : BddOrd} (f : X ⟶ Y) : - ofHom f.hom = f := rfl - @[simp] lemma ofHom_id {X : Type u} [PartialOrder X] [BoundedOrder X] : ofHom (BoundedOrderHom.id _) = 𝟙 (of X) := rfl diff --git a/Mathlib/Order/Category/BoolAlg.lean b/Mathlib/Order/Category/BoolAlg.lean index 2bd9e8a57f332d..b474b738cd98e6 100644 --- a/Mathlib/Order/Category/BoolAlg.lean +++ b/Mathlib/Order/Category/BoolAlg.lean @@ -42,42 +42,9 @@ instance : CoeSort BoolAlg (Type _) := attribute [coe] BoolAlg.carrier -set_option backward.privateInPublic true in -/-- The type of morphisms in `BoolAlg R`. -/ -@[ext] -structure Hom (X Y : BoolAlg.{u}) where - private mk :: - /-- The underlying `BoundedLatticeHom`. -/ - hom' : BoundedLatticeHom X Y - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category BoolAlg.{u} where - Hom X Y := Hom X Y - id X := ⟨BoundedLatticeHom.id X⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory BoolAlg (BoundedLatticeHom · ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `BoolAlg` back into a `BoundedLatticeHom`. -/ -abbrev Hom.hom {X Y : BoolAlg.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := BoolAlg) f - -/-- Typecheck a `BoundedLatticeHom` as a morphism in `BoolAlg`. -/ -abbrev ofHom {X Y : Type u} [BooleanAlgebra X] [BooleanAlgebra Y] (f : BoundedLatticeHom X Y) : - of X ⟶ of Y := - ConcreteCategory.ofHom (C := BoolAlg) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : BoolAlg.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category BoolAlg.{u} (BoundedLatticeHom · ·) BoundedLatticeHom.id BoundedLatticeHom.comp + with_of_hom {X Y : Type u} [BooleanAlgebra X] [BooleanAlgebra Y] + hom_type (BoundedLatticeHom X Y) from (of X) to (of Y) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. @@ -100,17 +67,10 @@ lemma ext {X Y : BoolAlg} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := -- This is not `simp` to avoid rewriting in types of terms. theorem coe_of (X : Type u) [BooleanAlgebra X] : (BoolAlg.of X : Type u) = X := rfl -@[simp] -lemma hom_id {X : BoolAlg} : (𝟙 X : X ⟶ X).hom = BoundedLatticeHom.id _ := rfl - /- Provided for rewriting. -/ lemma id_apply (X : BoolAlg) (x : X) : (𝟙 X : X ⟶ X) x = x := by simp -@[simp] -lemma hom_comp {X Y Z : BoolAlg} (f : X ⟶ Y) (g : Y ⟶ Z) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {X Y Z : BoolAlg} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp @@ -119,15 +79,6 @@ lemma comp_apply {X Y Z : BoolAlg} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : lemma hom_ext {X Y : BoolAlg} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {X Y : Type u} [BooleanAlgebra X] [BooleanAlgebra Y] (f : BoundedLatticeHom X Y) : - (ofHom f).hom = f := - rfl - -@[simp] -lemma ofHom_hom {X Y : BoolAlg} (f : X ⟶ Y) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {X : Type u} [BooleanAlgebra X] : ofHom (BoundedLatticeHom.id _) = 𝟙 (of X) := rfl diff --git a/Mathlib/Order/Category/DistLat.lean b/Mathlib/Order/Category/DistLat.lean index 53f247aa4385da..c0b142441f44c8 100644 --- a/Mathlib/Order/Category/DistLat.lean +++ b/Mathlib/Order/Category/DistLat.lean @@ -44,42 +44,10 @@ attribute [coe] DistLat.carrier /-- Construct a bundled `DistLat` from the underlying type and typeclass. -/ abbrev of (X : Type*) [DistribLattice X] : DistLat := ⟨X⟩ -set_option backward.privateInPublic true in -/-- The type of morphisms in `DistLat R`. -/ -@[ext] -structure Hom (X Y : DistLat.{u}) where - private mk :: - /-- The underlying `LatticeHom`. -/ - hom' : LatticeHom X Y - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category DistLat.{u} where - Hom X Y := Hom X Y - id X := ⟨LatticeHom.id X⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory DistLat (LatticeHom · ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `DistLat` back into a `LatticeHom`. -/ -abbrev Hom.hom {X Y : DistLat.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := DistLat) f - -/-- Typecheck a `LatticeHom` as a morphism in `DistLat`. -/ -abbrev ofHom {X Y : Type u} [DistribLattice X] [DistribLattice Y] (f : LatticeHom X Y) : - of X ⟶ of Y := - ConcreteCategory.ofHom (C := DistLat) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : DistLat.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category DistLat.{u} (LatticeHom · ·) (fun (X : DistLat) ↦ LatticeHom.id X) + LatticeHom.comp + with_of_hom {X Y : Type u} [DistribLattice X] [DistribLattice Y] + hom_type (LatticeHom X Y) from (of X) to (of Y) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. @@ -102,17 +70,10 @@ lemma ext {X Y : DistLat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := -- This is not `simp` to avoid rewriting in types of terms. theorem coe_of (X : Type u) [DistribLattice X] : (DistLat.of X : Type u) = X := rfl -@[simp] -lemma hom_id {X : DistLat} : (𝟙 X : X ⟶ X).hom = LatticeHom.id _ := rfl - /- Provided for rewriting. -/ lemma id_apply (X : DistLat) (x : X) : (𝟙 X : X ⟶ X) x = x := by simp -@[simp] -lemma hom_comp {X Y Z : DistLat} (f : X ⟶ Y) (g : Y ⟶ Z) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {X Y Z : DistLat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp @@ -121,15 +82,6 @@ lemma comp_apply {X Y Z : DistLat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : lemma hom_ext {X Y : DistLat} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {X Y : Type u} [DistribLattice X] [DistribLattice Y] (f : LatticeHom X Y) : - (ofHom f).hom = f := - rfl - -@[simp] -lemma ofHom_hom {X Y : DistLat} (f : X ⟶ Y) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {X : Type u} [DistribLattice X] : ofHom (LatticeHom.id _) = 𝟙 (of X) := rfl diff --git a/Mathlib/Order/Category/FinBddDistLat.lean b/Mathlib/Order/Category/FinBddDistLat.lean index 8a71f5e5a82168..1d26cb65387207 100644 --- a/Mathlib/Order/Category/FinBddDistLat.lean +++ b/Mathlib/Order/Category/FinBddDistLat.lean @@ -49,44 +49,12 @@ abbrev of' (α : Type*) [DistribLattice α] [Fintype α] [Nonempty α] : FinBddD carrier := α isBoundedOrder := Fintype.toBoundedOrder α -set_option backward.privateInPublic true in -/-- The type of morphisms in `FinBddDistLat R`. -/ -@[ext] -structure Hom (X Y : FinBddDistLat.{u}) where - private mk :: - /-- The underlying `BoundedLatticeHom`. -/ - hom' : BoundedLatticeHom X Y - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category FinBddDistLat.{u} where - Hom X Y := Hom X Y - id X := ⟨BoundedLatticeHom.id X⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory FinBddDistLat (BoundedLatticeHom · ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `FinBddDistLat` back into a `BoundedLatticeHom`. -/ -abbrev Hom.hom {X Y : FinBddDistLat.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := FinBddDistLat) f - -/-- Typecheck a `BoundedLatticeHom` as a morphism in `FinBddDistLat`. -/ -abbrev ofHom {X Y : Type u} [DistribLattice X] [BoundedOrder X] [Fintype X] [DistribLattice Y] - [BoundedOrder Y] [Fintype Y] - (f : BoundedLatticeHom X Y) : - of X ⟶ of Y := - ConcreteCategory.ofHom (C := FinBddDistLat) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : FinBddDistLat.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category FinBddDistLat.{u} (BoundedLatticeHom · ·) + (fun (X : FinBddDistLat) ↦ BoundedLatticeHom.id X) + BoundedLatticeHom.comp + with_of_hom {X Y : Type u} [DistribLattice X] [BoundedOrder X] [Fintype X] + [DistribLattice Y] [BoundedOrder Y] [Fintype Y] + hom_type (BoundedLatticeHom X Y) from (of X) to (of Y) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. @@ -106,17 +74,10 @@ lemma forget_map {X Y : FinBddDistLat} (f : X ⟶ Y) : lemma ext {X Y : FinBddDistLat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := ConcreteCategory.hom_ext _ _ w -@[simp] -lemma hom_id {X : FinBddDistLat} : (𝟙 X : X ⟶ X).hom = BoundedLatticeHom.id _ := rfl - /- Provided for rewriting. -/ lemma id_apply (X : FinBddDistLat) (x : X) : (𝟙 X : X ⟶ X) x = x := by simp -@[simp] -lemma hom_comp {X Y Z : FinBddDistLat} (f : X ⟶ Y) (g : Y ⟶ Z) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {X Y Z : FinBddDistLat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp @@ -125,14 +86,6 @@ lemma comp_apply {X Y Z : FinBddDistLat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : lemma hom_ext {X Y : FinBddDistLat} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {X Y : Type u} [DistribLattice X] [BoundedOrder X] [Fintype X] [DistribLattice Y] - [BoundedOrder Y] [Fintype Y] (f : BoundedLatticeHom X Y) : (ofHom f).hom = f := rfl - -@[simp] -lemma ofHom_hom {X Y : FinBddDistLat} (f : X ⟶ Y) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {X : Type u} [DistribLattice X] [BoundedOrder X] [Fintype X] : ofHom (BoundedLatticeHom.id _) = 𝟙 (of X) := rfl diff --git a/Mathlib/Order/Category/Frm.lean b/Mathlib/Order/Category/Frm.lean index 1d87b29e749074..6166e7ff0d0ced 100644 --- a/Mathlib/Order/Category/Frm.lean +++ b/Mathlib/Order/Category/Frm.lean @@ -45,41 +45,9 @@ instance : CoeSort Frm (Type _) := attribute [coe] Frm.carrier -set_option backward.privateInPublic true in -/-- The type of morphisms in `Frm R`. -/ -@[ext] -structure Hom (X Y : Frm.{u}) where - private mk :: - /-- The underlying `FrameHom`. -/ - hom' : FrameHom X Y - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category Frm.{u} where - Hom X Y := Hom X Y - id X := ⟨FrameHom.id X⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory Frm (FrameHom · ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `Frm` back into a `FrameHom`. -/ -abbrev Hom.hom {X Y : Frm.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := Frm) f - -/-- Typecheck a `FrameHom` as a morphism in `Frm`. -/ -abbrev ofHom {X Y : Type u} [Frame X] [Frame Y] (f : FrameHom X Y) : of X ⟶ of Y := - ConcreteCategory.ofHom (C := Frm) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : Frm.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category Frm.{u} (FrameHom · ·) (fun (X : Frm) ↦ FrameHom.id X) FrameHom.comp + with_of_hom {X Y : Type u} [Frame X] [Frame Y] + hom_type (FrameHom X Y) from (of X) to (of Y) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. @@ -102,17 +70,10 @@ lemma ext {X Y : Frm} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := -- This is not `simp` to avoid rewriting in types of terms. theorem coe_of (X : Type u) [Frame X] : (Frm.of X : Type u) = X := rfl -@[simp] -lemma hom_id {X : Frm} : (𝟙 X : X ⟶ X).hom = FrameHom.id _ := rfl - /- Provided for rewriting. -/ lemma id_apply (X : Frm) (x : X) : (𝟙 X : X ⟶ X) x = x := by simp -@[simp] -lemma hom_comp {X Y Z : Frm} (f : X ⟶ Y) (g : Y ⟶ Z) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {X Y Z : Frm} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp @@ -121,13 +82,6 @@ lemma comp_apply {X Y Z : Frm} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : lemma hom_ext {X Y : Frm} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {X Y : Type u} [Frame X] [Frame Y] (f : FrameHom X Y) : (ofHom f).hom = f := rfl - -@[simp] -lemma ofHom_hom {X Y : Frm} (f : X ⟶ Y) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {X : Type u} [Frame X] : ofHom (FrameHom.id _) = 𝟙 (of X) := rfl diff --git a/Mathlib/Order/Category/HeytAlg.lean b/Mathlib/Order/Category/HeytAlg.lean index 1d19ad5e2ede62..e5a072d3bc0f23 100644 --- a/Mathlib/Order/Category/HeytAlg.lean +++ b/Mathlib/Order/Category/HeytAlg.lean @@ -41,42 +41,10 @@ attribute [coe] HeytAlg.carrier /-- Construct a bundled `HeytAlg` from the underlying type and typeclass. -/ abbrev of (X : Type*) [HeytingAlgebra X] : HeytAlg := ⟨X⟩ -set_option backward.privateInPublic true in -/-- The type of morphisms in `HeytAlg R`. -/ -@[ext] -structure Hom (X Y : HeytAlg.{u}) where - private mk :: - /-- The underlying `HeytingHom`. -/ - hom' : HeytingHom X Y - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category HeytAlg.{u} where - Hom X Y := Hom X Y - id X := ⟨HeytingHom.id X⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory HeytAlg (HeytingHom · ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `HeytAlg` back into a `HeytingHom`. -/ -abbrev Hom.hom {X Y : HeytAlg.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := HeytAlg) f - -/-- Typecheck a `HeytingHom` as a morphism in `HeytAlg`. -/ -abbrev ofHom {X Y : Type u} [HeytingAlgebra X] [HeytingAlgebra Y] (f : HeytingHom X Y) : - of X ⟶ of Y := - ConcreteCategory.ofHom (C := HeytAlg) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : HeytAlg.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category HeytAlg.{u} (HeytingHom · ·) (fun (X : HeytAlg) ↦ HeytingHom.id X) + HeytingHom.comp + with_of_hom {X Y : Type u} [HeytingAlgebra X] [HeytingAlgebra Y] + hom_type (HeytingHom X Y) from (of X) to (of Y) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. @@ -99,17 +67,10 @@ lemma ext {X Y : HeytAlg} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := -- This is not `simp` to avoid rewriting in types of terms. theorem coe_of (X : Type u) [HeytingAlgebra X] : (HeytAlg.of X : Type u) = X := rfl -@[simp] -lemma hom_id {X : HeytAlg} : (𝟙 X : X ⟶ X).hom = HeytingHom.id _ := rfl - /- Provided for rewriting. -/ lemma id_apply (X : HeytAlg) (x : X) : (𝟙 X : X ⟶ X) x = x := by simp -@[simp] -lemma hom_comp {X Y Z : HeytAlg} (f : X ⟶ Y) (g : Y ⟶ Z) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {X Y Z : HeytAlg} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp @@ -118,15 +79,6 @@ lemma comp_apply {X Y Z : HeytAlg} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : lemma hom_ext {X Y : HeytAlg} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {X Y : Type u} [HeytingAlgebra X] [HeytingAlgebra Y] (f : HeytingHom X Y) : - (ofHom f).hom = f := - rfl - -@[simp] -lemma ofHom_hom {X Y : HeytAlg} (f : X ⟶ Y) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {X : Type u} [HeytingAlgebra X] : ofHom (HeytingHom.id _) = 𝟙 (of X) := rfl diff --git a/Mathlib/Order/Category/Lat.lean b/Mathlib/Order/Category/Lat.lean index 6e4dc11410bbe7..3caba7d2bb6f81 100644 --- a/Mathlib/Order/Category/Lat.lean +++ b/Mathlib/Order/Category/Lat.lean @@ -48,41 +48,9 @@ attribute [coe] Lat.carrier /-- Construct a bundled `Lat` from the underlying type and typeclass. -/ abbrev of (X : Type*) [Lattice X] : Lat := ⟨X⟩ -set_option backward.privateInPublic true in -/-- The type of morphisms in `Lat R`. -/ -@[ext] -structure Hom (X Y : Lat.{u}) where - private mk :: - /-- The underlying `LatticeHom`. -/ - hom' : LatticeHom X Y - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category Lat.{u} where - Hom X Y := Hom X Y - id X := ⟨LatticeHom.id X⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory Lat (LatticeHom · ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `Lat` back into a `LatticeHom`. -/ -abbrev Hom.hom {X Y : Lat.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := Lat) f - -/-- Typecheck a `LatticeHom` as a morphism in `Lat`. -/ -abbrev ofHom {X Y : Type u} [Lattice X] [Lattice Y] (f : LatticeHom X Y) : of X ⟶ of Y := - ConcreteCategory.ofHom (C := Lat) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : Lat.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category Lat.{u} (LatticeHom · ·) (fun (X : Lat) ↦ LatticeHom.id X) LatticeHom.comp + with_of_hom {X Y : Type u} [Lattice X] [Lattice Y] + hom_type (LatticeHom X Y) from (of X) to (of Y) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. @@ -105,17 +73,10 @@ lemma ext {X Y : Lat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := -- This is not `simp` to avoid rewriting in types of terms. theorem coe_of (X : Type u) [Lattice X] : (Lat.of X : Type u) = X := rfl -@[simp] -lemma hom_id {X : Lat} : (𝟙 X : X ⟶ X).hom = LatticeHom.id _ := rfl - /- Provided for rewriting. -/ lemma id_apply (X : Lat) (x : X) : (𝟙 X : X ⟶ X) x = x := by simp -@[simp] -lemma hom_comp {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp @@ -124,14 +85,6 @@ lemma comp_apply {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : lemma hom_ext {X Y : Lat} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {X Y : Type u} [Lattice X] [Lattice Y] (f : LatticeHom X Y) : (ofHom f).hom = f := - rfl - -@[simp] -lemma ofHom_hom {X Y : Lat} (f : X ⟶ Y) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {X : Type u} [Lattice X] : ofHom (LatticeHom.id _) = 𝟙 (of X) := rfl diff --git a/Mathlib/Order/Category/LinOrd.lean b/Mathlib/Order/Category/LinOrd.lean index 265092eefad930..40d320be64bc66 100644 --- a/Mathlib/Order/Category/LinOrd.lean +++ b/Mathlib/Order/Category/LinOrd.lean @@ -22,41 +22,9 @@ universe u namespace LinOrd -set_option backward.privateInPublic true in -/-- The type of morphisms in `LinOrd R`. -/ -@[ext] -structure Hom (X Y : LinOrd.{u}) where - private mk :: - /-- The underlying `OrderHom`. -/ - hom' : X →o Y - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category LinOrd.{u} where - Hom X Y := Hom X Y - id _ := ⟨OrderHom.id⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory LinOrd (· →o ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `LinOrd` back into a `OrderHom`. -/ -abbrev Hom.hom {X Y : LinOrd.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := LinOrd) f - -/-- Typecheck a `OrderHom` as a morphism in `LinOrd`. -/ -abbrev ofHom {X Y : Type u} [LinearOrder X] [LinearOrder Y] (f : X →o Y) : of X ⟶ of Y := - ConcreteCategory.ofHom (C := LinOrd) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : LinOrd.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category LinOrd.{u} (· →o ·) (fun (_ : LinOrd) ↦ OrderHom.id) OrderHom.comp + with_of_hom {X Y : Type u} [LinearOrder X] [LinearOrder Y] + hom_type (X →o Y) from (of X) to (of Y) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. @@ -79,17 +47,10 @@ lemma ext {X Y : LinOrd} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := -- This is not `simp` to avoid rewriting in types of terms. theorem coe_of (X : Type u) [LinearOrder X] : (LinOrd.of X : Type u) = X := rfl -@[simp] -lemma hom_id {X : LinOrd} : (𝟙 X : X ⟶ X).hom = OrderHom.id := rfl - /- Provided for rewriting. -/ lemma id_apply (X : LinOrd) (x : X) : (𝟙 X : X ⟶ X) x = x := by simp -@[simp] -lemma hom_comp {X Y Z : LinOrd} (f : X ⟶ Y) (g : Y ⟶ Z) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {X Y Z : LinOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp @@ -98,14 +59,6 @@ lemma comp_apply {X Y Z : LinOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : lemma hom_ext {X Y : LinOrd} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {X Y : Type u} [LinearOrder X] [LinearOrder Y] (f : X →o Y) : (ofHom f).hom = f := - rfl - -@[simp] -lemma ofHom_hom {X Y : LinOrd} (f : X ⟶ Y) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {X : Type u} [LinearOrder X] : ofHom OrderHom.id = 𝟙 (of X) := rfl diff --git a/Mathlib/Order/Category/PartOrd.lean b/Mathlib/Order/Category/PartOrd.lean index 986b64fcea5f52..119d951ba99aa8 100644 --- a/Mathlib/Order/Category/PartOrd.lean +++ b/Mathlib/Order/Category/PartOrd.lean @@ -40,41 +40,9 @@ instance : CoeSort PartOrd (Type _) := attribute [coe] PartOrd.carrier -set_option backward.privateInPublic true in -/-- The type of morphisms in `PartOrd R`. -/ -@[ext] -structure Hom (X Y : PartOrd.{u}) where - private mk :: - /-- The underlying `OrderHom`. -/ - hom' : X →o Y - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category PartOrd.{u} where - Hom X Y := Hom X Y - id _ := ⟨OrderHom.id⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory PartOrd (· →o ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `PartOrd` back into a `OrderHom`. -/ -abbrev Hom.hom {X Y : PartOrd.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := PartOrd) f - -/-- Typecheck a `OrderHom` as a morphism in `PartOrd`. -/ -abbrev ofHom {X Y : Type u} [PartialOrder X] [PartialOrder Y] (f : X →o Y) : of X ⟶ of Y := - ConcreteCategory.ofHom (C := PartOrd) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : PartOrd.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category PartOrd.{u} (· →o ·) (fun _ ↦ OrderHom.id) OrderHom.comp + with_of_hom {X Y : Type u} [PartialOrder X] [PartialOrder Y] + hom_type (X →o Y) from (of X) to (of Y) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. @@ -95,17 +63,10 @@ lemma ext {X Y : PartOrd} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := -- This is not `simp` to avoid rewriting in types of terms. theorem coe_of (X : Type u) [PartialOrder X] : (PartOrd.of X : Type u) = X := rfl -@[simp] -lemma hom_id {X : PartOrd} : (𝟙 X : X ⟶ X).hom = OrderHom.id := rfl - /- Provided for rewriting. -/ lemma id_apply (X : PartOrd) (x : X) : (𝟙 X : X ⟶ X) x = x := by simp -@[simp] -lemma hom_comp {X Y Z : PartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {X Y Z : PartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp @@ -114,13 +75,6 @@ lemma comp_apply {X Y Z : PartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : lemma hom_ext {X Y : PartOrd} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {X Y : Type u} [PartialOrder X] [PartialOrder Y] (f : X →o Y) : (ofHom f).hom = f := - rfl - -@[simp] -lemma ofHom_hom {X Y : PartOrd} (f : X ⟶ Y) : ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {X : Type u} [PartialOrder X] : ofHom OrderHom.id = 𝟙 (of X) := rfl diff --git a/Mathlib/Order/Category/PartOrdEmb.lean b/Mathlib/Order/Category/PartOrdEmb.lean index 7441fbffd968a9..a14edd143ff034 100644 --- a/Mathlib/Order/Category/PartOrdEmb.lean +++ b/Mathlib/Order/Category/PartOrdEmb.lean @@ -43,47 +43,14 @@ instance : CoeSort PartOrdEmb (Type _) := attribute [coe] PartOrdEmb.carrier -set_option backward.privateInPublic true in -/-- The type of morphisms in `PartOrdEmb R`. -/ -@[ext] -structure Hom (X Y : PartOrdEmb.{u}) where - private mk :: - /-- The underlying `OrderEmbedding`. -/ - hom' : X ↪o Y - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category PartOrdEmb.{u} where - Hom X Y := Hom X Y - id _ := ⟨RelEmbedding.refl _⟩ - comp f g := ⟨f.hom'.trans g.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory PartOrdEmb (· ↪o ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `PartOrdEmb` back into a `OrderEmbedding`. -/ -abbrev Hom.hom {X Y : PartOrdEmb.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := PartOrdEmb) f - -/-- Typecheck a `OrderEmbedding` as a morphism in `PartOrdEmb`. -/ -abbrev ofHom {X Y : Type u} [PartialOrder X] [PartialOrder Y] (f : X ↪o Y) : of X ⟶ of Y := - ConcreteCategory.ofHom (C := PartOrdEmb) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : PartOrdEmb.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category PartOrdEmb.{u} (· ↪o ·) (fun _ ↦ RelEmbedding.refl _) (fun g f ↦ f.trans g) + with_of_hom {X Y : Type u} [PartialOrder X] [PartialOrder Y] + hom_type (X ↪o Y) from (of X) to (of Y) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ -@[simp] lemma coe_id {X : PartOrdEmb} : (𝟙 X : X → X) = id := rfl @[simp] @@ -100,16 +67,10 @@ lemma ext {X Y : PartOrdEmb} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g -- This is not `simp` to avoid rewriting in types of terms. theorem coe_of (X : Type u) [PartialOrder X] : (PartOrdEmb.of X : Type u) = X := rfl -lemma hom_id {X : PartOrdEmb} : (𝟙 X : X ⟶ X).hom = RelEmbedding.refl _ := rfl - /- Provided for rewriting. -/ lemma id_apply (X : PartOrdEmb) (x : X) : (𝟙 X : X ⟶ X) x = x := by simp -@[simp] -lemma hom_comp {X Y Z : PartOrdEmb} (f : X ⟶ Y) (g : Y ⟶ Z) : - (f ≫ g).hom = f.hom.trans g.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {X Y Z : PartOrdEmb} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp @@ -125,14 +86,6 @@ lemma Hom.le_iff_le {X Y : PartOrdEmb.{u}} (f : X ⟶ Y) (x₁ x₂ : X) : lemma hom_ext {X Y : PartOrdEmb} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {X Y : Type u} [PartialOrder X] [PartialOrder Y] (f : X ↪o Y) : - (ofHom f).hom = f := - rfl - -@[simp] -lemma ofHom_hom {X Y : PartOrdEmb} (f : X ⟶ Y) : ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {X : Type u} [PartialOrder X] : ofHom (RelEmbedding.refl _) = 𝟙 (of X) := rfl diff --git a/Mathlib/Order/Category/Preord.lean b/Mathlib/Order/Category/Preord.lean index 760af02549d139..5d7ea4898267f7 100644 --- a/Mathlib/Order/Category/Preord.lean +++ b/Mathlib/Order/Category/Preord.lean @@ -10,6 +10,7 @@ public import Mathlib.CategoryTheory.Category.Preorder public import Mathlib.CategoryTheory.ConcreteCategory.Forget public import Mathlib.Order.Hom.Basic public import Mathlib.Order.CompleteBooleanAlgebra +public import Mathlib.Tactic.CategoryTheory.MkConcreteCategory /-! # Category of preorders @@ -43,41 +44,9 @@ instance : CoeSort Preord (Type u) := attribute [coe] Preord.carrier -set_option backward.privateInPublic true in -/-- The type of morphisms in `Preord R`. -/ -@[ext] -structure Hom (X Y : Preord.{u}) where - private mk :: - /-- The underlying `OrderHom`. -/ - hom' : X →o Y - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category Preord.{u} where - Hom X Y := Hom X Y - id _ := ⟨OrderHom.id⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory Preord (· →o ·) where - hom := Hom.hom' - ofHom := Hom.mk - -/-- Turn a morphism in `Preord` back into a `OrderHom`. -/ -abbrev Hom.hom {X Y : Preord.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := Preord) f - -/-- Typecheck a `OrderHom` as a morphism in `Preord`. -/ -abbrev ofHom {X Y : Type u} [Preorder X] [Preorder Y] (f : X →o Y) : of X ⟶ of Y := - ConcreteCategory.ofHom (C := Preord) f - -variable {R} in -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : Preord.{u}) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category Preord.{u} (· →o ·) (fun _ ↦ OrderHom.id) OrderHom.comp + with_of_hom {X Y : Type u} [Preorder X] [Preorder Y] + hom_type (X →o Y) from (of X) to (of Y) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. @@ -98,17 +67,10 @@ lemma ext {X Y : Preord} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := -- This is not `simp` to avoid rewriting in types of terms. theorem coe_of (X : Type u) [Preorder X] : (Preord.of X : Type u) = X := rfl -@[simp] -lemma hom_id {X : Preord} : (𝟙 X : X ⟶ X).hom = OrderHom.id := rfl - /- Provided for rewriting. -/ lemma id_apply (X : Preord) (x : X) : (𝟙 X : X ⟶ X) x = x := by simp -@[simp] -lemma hom_comp {X Y Z : Preord} (f : X ⟶ Y) (g : Y ⟶ Z) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ lemma comp_apply {X Y Z : Preord} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp @@ -117,12 +79,6 @@ lemma comp_apply {X Y Z : Preord} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : lemma hom_ext {X Y : Preord} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g := Hom.ext hf -@[simp] -lemma hom_ofHom {X Y : Type u} [Preorder X] [Preorder Y] (f : X →o Y) : (ofHom f).hom = f := rfl - -@[simp] -lemma ofHom_hom {X Y : Preord} (f : X ⟶ Y) : ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {X : Type u} [Preorder X] : ofHom OrderHom.id = 𝟙 (of X) := rfl diff --git a/Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean b/Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean index 9e0abfbb54948a..910c7f81d58b3d 100644 --- a/Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean +++ b/Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean @@ -403,7 +403,7 @@ instance mapCycles₁_quotientGroupMk'_epi : choose! s hs using QuotientGroup.mk_surjective (s := S) have hs₁ : QuotientGroup.mk ∘ s = id := funext hs refine ⟨⟨mapDomain s x, ?_⟩, Subtype.ext <| by - simp [mapCycles₁_hom, ← mapDomain_comp, hs₁, res, Rep.hom_id (of _)]⟩ + simp [mapCycles₁_hom, ← mapDomain_comp, hs₁, res, Rep.hom_id (X := of _)]⟩ simpa [mem_cycles₁_iff, ← (mem_cycles₁_iff _).1 hx, sum_mapDomain_index_inj (f := s) (fun x y h => by rw [← hs x, ← hs y, h])] using Finsupp.sum_congr fun a b => QuotientGroup.induction_on a fun a => by @@ -460,14 +460,14 @@ theorem H1CoresCoinfOfTrivial_exact : (d₂₁ (A.ofQuotient S)).hom y := by have := congr($((mapShortComplexH1 (QuotientGroup.mk' S) (resOfQuotientIso A S).inv).comm₁₂.symm) z) - simp_all [shortComplexH1, z, ← mapDomain_comp, Prod.map_comp_map, Rep.hom_id (res _ _)] + simp_all [shortComplexH1, z, ← mapDomain_comp, Prod.map_comp_map, Rep.hom_id (X := res _ _)] let v := x - (d₂₁ _).hom z /- We have `C₁(s ∘ π)(v) = ∑ v(g)·s(π(g)) = 0`, since `C₁(π)(v) = dC₁(π)(z) - C₁(π)(dz) = 0` by previous assumptions. -/ have hv : mapDomain (s ∘ QuotientGroup.mk) v = 0 := by rw [mapDomain_comp] simp only [QuotientGroup.coe_mk', lmapDomain_apply, mapDomain_sub, v] at hz ⊢ - simp [hz, hy, coe_mapCycles₁ (QuotientGroup.mk' S), Rep.hom_id (of _)] + simp [hz, hy, coe_mapCycles₁ (QuotientGroup.mk' S), Rep.hom_id (X := of _)] let e : G → G × G := fun (g : G) => (s (g : G ⧸ S), (s (g : G ⧸ S))⁻¹ * g) have he : e.Injective := fun x y hxy => by obtain ⟨(h₁ : s _ = s _), (h₂ : _ * _ = _ * _)⟩ := Prod.ext_iff.1 hxy @@ -579,7 +579,7 @@ and `Y - ∑ aᵢ·sᵢ` is a cycle. -/ /- Moreover, the image of `Y - ∑ aᵢ·sᵢ` in `Z₁(G ⧸ S, A_S)` is `x - ∑ aᵢ·1`, and hence differs from `x` by a boundary, since `aᵢ·1 = d(aᵢ·(1, 1))`. -/ refine (H1π_eq_iff _ _).2 ?_ - simpa [← hy, mapCycles₁_hom, map_sub, Rep.hom_id (res _ _), ← mapDomain_comp, + simpa [← hy, mapCycles₁_hom, map_sub, Rep.hom_id (X := res _ _), ← mapDomain_comp, ← mapDomain_mapRange, hY, Function.comp_def, (QuotientGroup.eq_one_iff <| Subtype.val _).2 (Subtype.prop _)] using Submodule.finsuppSum_mem _ _ _ _ fun _ _ ↦ single_one_mem_boundaries₁ _ diff --git a/Mathlib/RepresentationTheory/Rep/Basic.lean b/Mathlib/RepresentationTheory/Rep/Basic.lean index d27c5342cd6996..a65826ceb7f560 100644 --- a/Mathlib/RepresentationTheory/Rep/Basic.lean +++ b/Mathlib/RepresentationTheory/Rep/Basic.lean @@ -67,52 +67,19 @@ lemma of_V : (of ρ).V = X := by with_reducible rfl variable (X ρ) in lemma of_ρ : (of ρ).ρ = ρ := by with_reducible rfl -set_option backward.privateInPublic true in -/-- The type of morphisms in `Rep.{w} k G`. -/ -@[ext] -structure Hom where - private mk :: - /-- The underlying `G`-equivariant linear map. -/ - hom' : A.ρ.IntertwiningMap B.ρ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : Category (Rep.{w} k G) where - Hom A B := Hom A B - id A := ⟨.id A.ρ⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -instance : ConcreteCategory (Rep.{w} k G) (fun A B ↦ A.ρ.IntertwiningMap B.ρ) where - hom := Hom.hom' - ofHom := Hom.mk - -variable {A B} in -/-- Turn a morphism in `Rep` back into an `IntertwiningMap`. -/ -abbrev Hom.hom (f : Hom A B) := ConcreteCategory.hom (C := Rep k G) f - -variable {A B} in -/-- Typecheck an `IntertwiningMap` as a morphism in `Rep`. -/ -abbrev ofHom (f : ρ.IntertwiningMap σ) : of ρ ⟶ of σ := - ConcreteCategory.ofHom (C := Rep.{w} k G) f - -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (f : Hom A B) := f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category (Rep.{w} k G) (fun A B ↦ A.ρ.IntertwiningMap B.ρ) + (fun A ↦ Representation.IntertwiningMap.id A.ρ) (fun g f ↦ g.comp f) + with_of_hom {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] + {ρ : Representation k G X} {σ : Representation k G Y} + hom_type (ρ.IntertwiningMap σ) from (of ρ) to (of σ) /- The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ -@[simp] lemma hom_id : (𝟙 A : A ⟶ A).hom = .id A.ρ := rfl - /- Provided for rewriting. -/ lemma id_apply (a : A) : (𝟙 A : A ⟶ A) a = a := by simp [Representation.IntertwiningMap.id] -@[simp] lemma hom_comp (f : A ⟶ B) (g : B ⟶ C) : (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ variable {A B C} in lemma comp_apply (f : A ⟶ B) (g : B ⟶ C) (a : A) : (f ≫ g) a = g (f a) := by simp @@ -126,9 +93,6 @@ lemma hom_comm_apply (f : A ⟶ B) (g : G) (a : A) : f.hom (A.ρ g a) = B.ρ g ( variable {Z : Type w} [AddCommGroup Z] [Module k Z] {τ : Representation k G Z} -@[simp] lemma hom_ofHom (f : ρ.IntertwiningMap σ) : (ofHom f).hom = f := rfl -@[simp] lemma ofHom_hom (f : A ⟶ B) : ofHom f.hom = f := rfl - @[simp] lemma ofHom_id : ofHom (.id σ) = 𝟙 (of σ) := rfl @[simp] diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean index d66d693ade5d3d..44e29f901000b6 100644 --- a/Mathlib/Tactic.lean +++ b/Mathlib/Tactic.lean @@ -39,6 +39,7 @@ public import Mathlib.Tactic.CategoryTheory.Coherence.Normalize public import Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence public import Mathlib.Tactic.CategoryTheory.Elementwise public import Mathlib.Tactic.CategoryTheory.IsoReassoc +public import Mathlib.Tactic.CategoryTheory.MkConcreteCategory public import Mathlib.Tactic.CategoryTheory.Monoidal.Basic public import Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes public import Mathlib.Tactic.CategoryTheory.Monoidal.Normalize diff --git a/Mathlib/Tactic/CategoryTheory/MkConcreteCategory.lean b/Mathlib/Tactic/CategoryTheory/MkConcreteCategory.lean new file mode 100644 index 00000000000000..cbb860c5b7b87e --- /dev/null +++ b/Mathlib/Tactic/CategoryTheory/MkConcreteCategory.lean @@ -0,0 +1,469 @@ +/- +Copyright (c) 2026 Dagur Asgeirsson. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Dagur Asgeirsson +-/ +module + +public import Mathlib.CategoryTheory.ConcreteCategory.Basic +public import Mathlib.Tactic.ToAdditive + +/-! +# The `mk_concrete_category` command + +`mk_concrete_category C FC id comp` generates the standard initial boilerplate for a concrete +category whose morphisms are modeled by a bundled function type `FC`. The identity term is expected +to be of the form `(X : C) → FC X X` and the composition term is expected to be of the form +`{X Y Z : C} → FC Y Z → FC X Y → FC X Z`. + +The command is intended to be run in the namespace of the category it is defining. It creates a +one-field structure `Hom` which wraps a term of `FC`, with private field `Hom.hom'`, and uses it as +the type of morphisms in the category. It then creates: + +* `instCategory`, the `Category` instance with `id X = id X` and + `comp f g = comp g.hom' f.hom'`; +* `instConcreteCategory`, the `ConcreteCategory C FC` instance; +* `Hom.hom`, an abbreviation for the `ConcreteCategory.hom` projection from morphisms to `FC`; +* `Hom.Simps.hom`, so `simps` uses the public projection `hom` instead of the private `hom'`; +* `ofHom`, a public abbreviation for `ConcreteCategory.ofHom`; +* dsimp lemmas `hom_id`, `hom_comp`, `hom_ofHom`, and `ofHom_hom`. + +For example, the code + +```lean +structure TestCat where + α : Type u + +namespace TestCat + +@[ext] +structure Fun (X Y : TestCat.{u}) where + toFun : X.α → Y.α + +instance (X Y : TestCat.{u}) : FunLike (Fun X Y) X.α Y.α where + coe := Fun.toFun + coe_injective' _ _ _ := by aesop + +protected def Fun.id (X : TestCat.{u}) : Fun X X where + toFun := id + +protected def Fun.comp {X Y Z : TestCat.{u}} (g : Fun Y Z) (f : Fun X Y) : Fun X Z where + toFun := g.toFun ∘ f.toFun + +mk_concrete_category TestCat Fun Fun.id Fun.comp +``` + +generates an API where +`Hom.hom : X.Hom Y → X.Fun Y`, `ofHom : X.Fun Y → (X ⟶ Y)`, +`hom_id : Hom.hom (𝟙 X) = Fun.id X`, and +`hom_comp : Hom.hom (f ≫ g) = Fun.comp (Hom.hom g) (Hom.hom f)`. + +For bundled categories whose public constructor should take unbundled objects, `with_of_hom` +customizes the generated `ofHom` and `hom_ofHom`. + +```lean +variable (R : Type u) [Ring R] + +structure ModuleTestCat where + carrier : Type v + [isAddCommGroup : AddCommGroup carrier] + [isModule : Module R carrier] + +attribute [instance] ModuleTestCat.isAddCommGroup +attribute [instance 1100] ModuleTestCat.isModule + +namespace ModuleTestCat + +abbrev of (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] : + ModuleTestCat R := + ⟨M⟩ + +instance : CoeSort (ModuleTestCat.{v} R) (Type v) := + ⟨ModuleTestCat.carrier⟩ + +attribute [coe] ModuleTestCat.carrier + +variable {R} in +mk_concrete_category (ModuleTestCat.{v} R) (· →ₗ[R] ·) (@LinearMap.id R ·) LinearMap.comp + with_of_hom {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] + hom_type (X →ₗ[R] Y) from (of R X) to (of R Y) +``` + +Here `ofHom` has type `(X →ₗ[R] Y) → (of R X ⟶ of R Y)`, while `hom_comp` states +`Hom.hom (f ≫ g) = LinearMap.comp (Hom.hom g) (Hom.hom f)`. + +The identity and composition terms are ordinary Lean terms. Because categorical composition +`f ≫ g` is implemented as `comp g.hom' f.hom'`, the supplied `comp` should take the target-side +morphism first and the source-side morphism second. Placeholder abstractions such as +`LinearMap.comp · ·` keep Lean's usual argument order, which is exactly the order used by the +command. + +The explicit `to_additive` forms are for pairs of categories where the multiplicative and additive +versions should be generated at the same time. They take the multiplicative category data and the +corresponding additive category data in one command. The elaborator first enters the additive +namespace and generates the additive concrete category, then enters the multiplicative namespace and +generates the multiplicative one. This is useful for commands such as the test case generating both +`MultiplicativeTestCat` with homs `X →* Y` and `AdditiveTestCat` with homs `X →+ Y`, including their +matching `ofHom`, `hom_id`, and `hom_comp` declarations: + +```lean +structure AdditiveTestCat where + carrier : Type u + [str : AddMonoid carrier] + +@[to_additive AdditiveTestCat] +structure MultiplicativeTestCat where + carrier : Type u + [str : Monoid carrier] + +attribute [instance] AdditiveTestCat.str MultiplicativeTestCat.str + +namespace MultiplicativeTestCat + +@[to_additive] +abbrev of (M : Type u) [Monoid M] : MultiplicativeTestCat := + ⟨M⟩ + +@[to_additive instCoeSortAdditiveTestCat] +instance instCoeSort : CoeSort MultiplicativeTestCat (Type u) := + ⟨MultiplicativeTestCat.carrier⟩ + +end MultiplicativeTestCat + +attribute [coe] AdditiveTestCat.carrier MultiplicativeTestCat.carrier + +@[to_additive AdditiveTestCat] +mk_concrete_category MultiplicativeTestCat.{u} (· →* ·) MonoidHom.id MonoidHom.comp + with_of_hom {X Y : Type u} [Monoid X] [Monoid Y] + hom_type (X →* Y) from (MultiplicativeTestCat.of X) to (MultiplicativeTestCat.of Y) + to_additive AdditiveTestCat.{u} (· →+ ·) AddMonoidHom.id AddMonoidHom.comp + with_of_hom {X Y : Type u} [AddMonoid X] [AddMonoid Y] + hom_type (X →+ Y) from (AdditiveTestCat.of X) to (AdditiveTestCat.of Y) +``` +-/ + +open Lean Elab Command Term Meta +open CategoryTheory + +namespace Mathlib.Tactic.CategoryTheory + +/-! +The parser exposes four surface forms: the basic command, the same command with a custom `ofHom` +signature, a form that supplies multiplicative and additive category data together, and a combined +form with both `with_of_hom` and explicit additive data. +-/ + +/-- +`mk_concrete_category C FC id comp` generates the standard boilerplate for a concrete category on +`C` whose underlying bundled hom type is `FC : C → C → Type*`, with identities given by `id X` +and composition given by `comp g.hom' f.hom'` for categorical morphisms `f : X ⟶ Y` and +`g : Y ⟶ Z`. + +The command is intended to be used in the namespace of `C`. It creates declarations named `Hom`, +`Hom.hom`, `ofHom`, `hom_id`, `hom_comp`, `hom_ofHom`, and `ofHom_hom`. +-/ +syntax (name := mkConcreteCategory) declModifiers "mk_concrete_category " term:max ppSpace + term:max ppSpace term:max ppSpace term:max : command + +/-- Variant of `mk_concrete_category` with a custom generated `ofHom` signature. -/ +syntax (name := mkConcreteCategoryWithOfHom) declModifiers "mk_concrete_category " term:max ppSpace + term:max ppSpace term:max ppSpace term:max ppSpace "with_of_hom" + (ppSpace bracketedBinder)* ppSpace "hom_type " term:max ppSpace "from " term:max ppSpace + "to " term:max : command + +/-- Variant of `mk_concrete_category` generating multiplicative and additive categories together. -/ +syntax (name := mkConcreteCategoryWithAdditive) declModifiers + "mk_concrete_category " term:max ppSpace term:max ppSpace term:max ppSpace term:max ppSpace + "to_additive " term:max ppSpace term:max ppSpace term:max ppSpace term:max : command + +/-- Variant of `mk_concrete_category` combining the custom `ofHom` and additive forms. -/ +syntax (name := mkConcreteCategoryWithOfHomAndAdditive) (priority := high) declModifiers + "mk_concrete_category " term:max ppSpace term:max ppSpace term:max ppSpace term:max ppSpace + "with_of_hom" (ppSpace bracketedBinder)* ppSpace "hom_type " term:max ppSpace + "from " term:max ppSpace "to " term:max ppSpace + "to_additive " term:max ppSpace term:max ppSpace term:max ppSpace term:max ppSpace + "with_of_hom" (ppSpace bracketedBinder)* ppSpace "hom_type " term:max ppSpace + "from " term:max ppSpace "to " term:max : command + +/-! +These helpers inspect raw syntax rather than elaborated terms. This command has to notice ordinary +command modifiers such as `@[to_additive]` before Lean elaborates them. +-/ + +/-- Whether a syntax tree contains a `to_additive` attribute. -/ +private meta partial def hasToAdditiveAttr (stx : Syntax) : Bool := + match stx with + | .ident _ _ n _ => n == `to_additive + | .atom _ val => val == "to_additive" + | .node _ k args => k == ``Mathlib.Tactic.ToAdditive.to_additive || args.any hasToAdditiveAttr + | _ => false + +/-- The first identifier occurring in a syntax tree. -/ +private meta partial def firstIdent? (stx : Syntax) : Option Name := + if stx.isIdent then some stx.getId else + match stx with + | .node _ _ args => args.findSome? firstIdent? + | _ => none + +/-- The explicit target of a `@[to_additive Target]` attribute, if present. -/ +private meta partial def toAdditiveTarget? (stx : Syntax) : Option Name := + if stx.isOfKind ``Mathlib.Tactic.ToAdditive.to_additive then + firstIdent? stx + else + match stx with + | .node _ _ args => args.findSome? toAdditiveTarget? + | _ => none + +/-! +The explicit `to_additive` forms generate declarations by entering the target namespaces and +running the same core generator there. These helpers keep the namespace checks and open/close +commands in one place. +-/ + +/-- The head identifier of a term, allowing explicit universe syntax such as `C.{u}`. -/ +private meta partial def headTermIdent? (stx : Syntax) : Option Name := + if stx.isIdent then + some stx.getId + else + match stx with + | .node _ k args => + if k == ``Lean.Parser.Term.explicitUniv then + args[0]?.bind headTermIdent? + else + none + | _ => none + +/-- Turn a category term from a `to_additive` form into the namespace identifier to generate in. -/ +private meta def categoryNamespaceIdent (cat : TSyntax `term) (message : String) : + CommandElabM Ident := do + if let some n := headTermIdent? cat.raw then + pure <| mkIdent n + else + throwErrorAt cat message + +/-- Elaborate commands inside a namespace generated by a `to_additive` form. -/ +private meta def elabInNamespace (ns : Ident) (body : CommandElabM Unit) : CommandElabM Unit := do + elabCommand <| ← set_option hygiene false in `(command| namespace $ns:ident) + body + elabCommand <| ← set_option hygiene false in `(command| end $ns:ident) + +/-- Register that a declaration generated on the multiplicative side has an existing additive +counterpart generated by the explicit `to_additive` form. -/ +private meta def registerToAdditiveExisting (src tgt : Name) : CommandElabM Unit := do + let srcIdent := mkIdent src + let tgtIdent := mkIdent tgt + elabCommand <| ← set_option hygiene false in + `(command| + set_option linter.translateGenerateName false in + set_option linter.existingAttributeWarning false in + attribute [to_additive existing $tgtIdent:ident] $srcIdent:ident) + +/-- Register the standard declarations generated by `mk_concrete_category` with `to_additive`, so +later `@[to_additive]` declarations can translate references to them. -/ +private meta def registerConcreteCategoryToAdditive (catNs addCatNs : Name) : + CommandElabM Unit := do + for suffix in [`Hom, `instCategory, `instConcreteCategory, `Hom.hom, `ofHom, + `Hom.Simps.hom, `hom_id, `hom_comp, `hom_ofHom, `ofHom_hom] do + registerToAdditiveExisting (catNs ++ suffix) (addCatNs ++ suffix) + +/-! +For the explicit `to_additive` form without `with_of_hom`, generation is just two ordinary +`mk_concrete_category` commands: one in the additive namespace, then one in the multiplicative +namespace. The additive side is generated first so any later `to_additive` naming choices on the +multiplicative side can refer to existing additive declarations. +-/ + +/-- Elaborator for the `mk_concrete_category ... to_additive ...` form. -/ +@[command_elab mkConcreteCategoryWithAdditive] +public meta def elabMkConcreteCategoryWithAdditive : CommandElab := fun stx => do + let `($_mods:declModifiers mk_concrete_category $cat $FC $idTerm $compTerm to_additive + $addCat $addFC $addIdTerm $addCompTerm) := stx + | throwUnsupportedSyntax + let catNs ← categoryNamespaceIdent cat "category must be an identifier in the `to_additive` form" + let addCatNs ← categoryNamespaceIdent addCat "additive category must be an identifier" + elabInNamespace addCatNs do + elabCommand <| ← set_option hygiene false in + `(command| mk_concrete_category $addCat $addFC $addIdTerm $addCompTerm) + elabInNamespace catNs do + elabCommand <| ← set_option hygiene false in + `(command| mk_concrete_category $cat $FC $idTerm $compTerm) + registerConcreteCategoryToAdditive catNs.getId addCatNs.getId + +/-- Data for a custom generated `ofHom` declaration: binders, source hom type, source +object, and target object. -/ +private abbrev CustomOfHomData := + TSyntaxArray `Lean.Parser.Term.bracketedBinder × TSyntax `term × TSyntax `term × TSyntax `term + +/-- Elaborate a term and beta-reduce it before storing it in a declaration type. -/ +syntax (name := mkConcreteCategoryBeta) "mk_concrete_category_beta% " term : term + +@[term_elab mkConcreteCategoryBeta, inherit_doc mkConcreteCategoryBeta] +public meta def elabMkConcreteCategoryBeta : TermElab := fun stx expectedType => do + Core.betaReduce (← instantiateMVars (← Term.elabTerm stx[1] expectedType)) + +/-! +The core generator emits the declarations shared by all forms: `Hom`, the category and concrete +category instances, projections and constructors, simps support, and the round-trip lemmas. Most +branches below differ only in attributes, so the generated syntax is kept explicit to make the +resulting declarations predictable. +-/ + +/-- Core implementation of `mk_concrete_category`. -/ +private meta def elabMkConcreteCategoryCore (mods : Syntax) (cat FC idTerm compTerm : TSyntax `term) + (customOfHom? : Option CustomOfHomData) : CommandElabM Unit := do + let useToAdditive := hasToAdditiveAttr mods + let addHom? := toAdditiveTarget? mods |>.map fun n => mkCIdent (n ++ `Hom) + let addToAdditiveAttr (decl : Ident) : CommandElabM Unit := do + if useToAdditive then + elabCommand <| ← set_option hygiene false in + `(command| attribute [to_additive] $decl:ident) + let addSimpAttrs (decl : Ident) : CommandElabM Unit := do + if useToAdditive then + elabCommand <| ← set_option hygiene false in + `(command| attribute [to_additive (attr := simp), simp] $decl:ident) + else + elabCommand <| ← set_option hygiene false in + `(command| attribute [simp] $decl:ident) + + elabCommand <| ← set_option hygiene false in `(command| + set_option backward.privateInPublic true in + /-- The type of morphisms in this concrete category. -/ + structure Hom (X Y : $cat) where + private mk :: + /-- The underlying bundled morphism. -/ + hom' : ($FC : $cat → $cat → Type _) X Y) + match addHom? with + | some addHom => + elabCommand <| ← set_option hygiene false in + `(command| attribute [to_additive $addHom:ident, ext] Hom) + | none => + if useToAdditive then + elabCommand <| ← set_option hygiene false in + `(command| attribute [to_additive, ext] Hom) + else + elabCommand <| ← set_option hygiene false in + `(command| attribute [ext] Hom) + + elabCommand <| ← set_option hygiene false in `(command| + set_option backward.privateInPublic true in + set_option backward.privateInPublic.warn false in + instance instCategory : CategoryTheory.Category $cat where + Hom X Y := Hom (X := X) (Y := Y) + id X := Hom.mk (X := X) (Y := X) (($idTerm) X) + comp {X Y Z} f g := Hom.mk (X := X) (Y := Z) (($compTerm) g.hom' f.hom')) + addToAdditiveAttr (mkIdent `instCategory) + + elabCommand <| ← set_option hygiene false in `(command| + set_option backward.privateInPublic true in + set_option backward.privateInPublic.warn false in + instance instConcreteCategory : + CategoryTheory.ConcreteCategory $cat ($FC : $cat → $cat → Type _) where + hom := fun f => Hom.hom' f + ofHom := fun {X Y} f => Hom.mk (X := X) (Y := Y) f + id_apply := by intros; rfl + comp_apply := by intros; rfl) + addToAdditiveAttr (mkIdent `instConcreteCategory) + + elabCommand <| ← set_option hygiene false in `(command| + /-- Turn a categorical morphism back into its underlying bundled morphism. -/ + abbrev Hom.hom {X Y : $cat} (f : X ⟶ Y) := + CategoryTheory.ConcreteCategory.hom (C := $cat) f) + addToAdditiveAttr (mkIdent `Hom.hom) + + match customOfHom? with + | some (binders, homTy, source, target) => + elabCommand <| ← set_option hygiene false in `(command| + /-- Typecheck a bundled morphism as a morphism in this concrete category. -/ + abbrev ofHom $binders:bracketedBinder* + (f : ($homTy)) : $source ⟶ $target := + CategoryTheory.ConcreteCategory.ofHom (C := $cat) f) + | none => + elabCommand <| ← set_option hygiene false in `(command| + /-- Typecheck a bundled morphism as a morphism in this concrete category. -/ + abbrev ofHom {X Y : $cat} (f : ($FC : $cat → $cat → Type _) X Y) : X ⟶ Y := + CategoryTheory.ConcreteCategory.ofHom (C := $cat) f) + addToAdditiveAttr (mkIdent `ofHom) + + elabCommand <| ← set_option hygiene false in `(command| + /-- Use the public `Hom.hom` projection for `@[simps]` lemmas. -/ + def Hom.Simps.hom : (X : $cat) → (Y : $cat) → Hom (X := X) (Y := Y) → + ($FC : $cat → $cat → Type _) X Y := + fun _ _ f => Hom.hom f) + addToAdditiveAttr (mkIdent `Hom.Simps.hom) + + elabCommand <| ← set_option hygiene false in `(command| + initialize_simps_projections Hom (hom' → hom)) + if let some addHom := addHom? then + elabCommand <| ← set_option hygiene false in `(command| + initialize_simps_projections $addHom:ident (hom' → hom)) + + elabCommand <| ← set_option hygiene false in `(command| + lemma hom_id {X : $cat} : + (𝟙 X : X ⟶ X).hom = mk_concrete_category_beta% (($idTerm) X) := + rfl) + addSimpAttrs (mkIdent `hom_id) + + elabCommand <| ← set_option hygiene false in `(command| + lemma hom_comp {X Y Z : $cat} (f : X ⟶ Y) (g : Y ⟶ Z) : + (f ≫ g).hom = mk_concrete_category_beta% (($compTerm) g.hom f.hom) := + rfl) + addSimpAttrs (mkIdent `hom_comp) + + match customOfHom? with + | some (binders, homTy, _, _) => + elabCommand <| ← set_option hygiene false in `(command| + lemma hom_ofHom $binders:bracketedBinder* (f : ($homTy)) : (ofHom f).hom = f := + rfl) + | none => + elabCommand <| ← set_option hygiene false in `(command| + lemma hom_ofHom {X Y : $cat} (f : ($FC : $cat → $cat → Type _) X Y) : + (CategoryTheory.ConcreteCategory.ofHom (C := $cat) f).hom = f := + rfl) + addSimpAttrs (mkIdent `hom_ofHom) + + elabCommand <| ← set_option hygiene false in `(command| + lemma ofHom_hom {X Y : $cat} (f : X ⟶ Y) : + CategoryTheory.ConcreteCategory.ofHom (C := $cat) f.hom = f := + rfl) + addSimpAttrs (mkIdent `ofHom_hom) + +/-! +The remaining elaborators parse their surface syntax and delegate to the core generator. The +combined `with_of_hom`/`to_additive` form calls the core generator directly for each namespace +because each side has its own custom `ofHom` binders and source/target terms. +-/ + +/-- Elaborator for `mk_concrete_category`. -/ +@[command_elab mkConcreteCategory] +public meta def elabMkConcreteCategory : CommandElab := fun stx => do + let `($mods:declModifiers mk_concrete_category $cat $FC $idTerm $compTerm) := stx + | throwUnsupportedSyntax + elabMkConcreteCategoryCore mods cat FC idTerm compTerm none + +/-- Elaborator for the `mk_concrete_category ... with_of_hom ...` form. -/ +@[command_elab mkConcreteCategoryWithOfHom] +public meta def elabMkConcreteCategoryWithOfHom : CommandElab := fun stx => do + let `($mods:declModifiers mk_concrete_category $cat $FC $idTerm $compTerm with_of_hom + $binders:bracketedBinder* hom_type $homTy from $source to $target) := stx + | throwUnsupportedSyntax + elabMkConcreteCategoryCore mods cat FC idTerm compTerm (some (binders, homTy, source, target)) + +/-- Elaborator for the `mk_concrete_category ... with_of_hom ... to_additive ...` form. -/ +@[command_elab mkConcreteCategoryWithOfHomAndAdditive] +public meta def elabMkConcreteCategoryWithOfHomAndAdditive : CommandElab := fun stx => do + let `($_mods:declModifiers mk_concrete_category $cat $FC $idTerm $compTerm with_of_hom + $binders:bracketedBinder* hom_type $homTy from $source to $target to_additive + $addCat $addFC $addIdTerm $addCompTerm with_of_hom $addBinders:bracketedBinder* + hom_type $addHomTy from $addSource to $addTarget) := stx + | throwUnsupportedSyntax + let catNs ← categoryNamespaceIdent cat "category must be an identifier in the `to_additive` form" + let addCatNs ← categoryNamespaceIdent addCat "additive category must be an identifier" + elabInNamespace addCatNs do + elabMkConcreteCategoryCore Syntax.missing addCat addFC addIdTerm addCompTerm + (some (addBinders, addHomTy, addSource, addTarget)) + elabInNamespace catNs do + elabMkConcreteCategoryCore Syntax.missing cat FC idTerm compTerm + (some (binders, homTy, source, target)) + registerConcreteCategoryToAdditive catNs.getId addCatNs.getId + +end Mathlib.Tactic.CategoryTheory diff --git a/Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean b/Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean index d9d772218efd43..8ec96213c6b373 100644 --- a/Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean +++ b/Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean @@ -90,48 +90,17 @@ lemma ProfiniteGrp.coe_of (G : Type u) [Group G] [TopologicalSpace G] [IsTopolog [CompactSpace G] [TotallyDisconnectedSpace G] : (ProfiniteGrp.of G : Type u) = G := rfl -/-- The type of morphisms in `ProfiniteAddGrp`. -/ -@[ext] -structure ProfiniteAddGrp.Hom (A B : ProfiniteAddGrp.{u}) where - private mk :: - /-- The underlying `ContinuousAddMonoidHom`. -/ - hom' : A →ₜ+ B - -/-- The type of morphisms in `ProfiniteGrp`. -/ -@[to_additive existing (attr := ext)] -structure ProfiniteGrp.Hom (A B : ProfiniteGrp.{u}) where - private mk :: - /-- The underlying `ContinuousMonoidHom`. -/ - hom' : A →ₜ* B - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -@[to_additive] -instance : Category ProfiniteGrp where - Hom A B := ProfiniteGrp.Hom A B - id A := ⟨ContinuousMonoidHom.id A⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -set_option backward.privateInPublic true in -set_option backward.privateInPublic.warn false in -@[to_additive] -instance : ConcreteCategory ProfiniteGrp (fun X Y => X →ₜ* Y) where - hom f := f.hom' - ofHom f := ⟨f⟩ - -/-- The underlying `ContinuousMonoidHom`. -/ -@[to_additive /-- The underlying `ContinuousAddMonoidHom`. -/] -abbrev ProfiniteGrp.Hom.hom {M N : ProfiniteGrp.{u}} (f : ProfiniteGrp.Hom M N) : - M →ₜ* N := - ConcreteCategory.hom (C := ProfiniteGrp) f - -/-- Typecheck a `ContinuousMonoidHom` as a morphism in `ProfiniteGrp`. -/ -@[to_additive /-- Typecheck a `ContinuousAddMonoidHom` as a morphism in `ProfiniteAddGrp`. -/] -abbrev ProfiniteGrp.ofHom {X Y : Type u} [Group X] [TopologicalSpace X] [IsTopologicalGroup X] - [CompactSpace X] [TotallyDisconnectedSpace X] [Group Y] [TopologicalSpace Y] - [IsTopologicalGroup Y] [CompactSpace Y] [TotallyDisconnectedSpace Y] - (f : X →ₜ* Y) : ProfiniteGrp.of X ⟶ ProfiniteGrp.of Y := - ConcreteCategory.ofHom f +@[to_additive ProfiniteAddGrp] +mk_concrete_category ProfiniteGrp.{u} (· →ₜ* ·) ContinuousMonoidHom.id ContinuousMonoidHom.comp + with_of_hom {X Y : Type u} [Group X] [TopologicalSpace X] [IsTopologicalGroup X] + [CompactSpace X] [TotallyDisconnectedSpace X] [Group Y] [TopologicalSpace Y] + [IsTopologicalGroup Y] [CompactSpace Y] [TotallyDisconnectedSpace Y] + hom_type (X →ₜ* Y) from (ProfiniteGrp.of X) to (ProfiniteGrp.of Y) + to_additive ProfiniteAddGrp.{u} (· →ₜ+ ·) ContinuousAddMonoidHom.id ContinuousAddMonoidHom.comp + with_of_hom {X Y : Type u} [AddGroup X] [TopologicalSpace X] [IsTopologicalAddGroup X] + [CompactSpace X] [TotallyDisconnectedSpace X] [AddGroup Y] [TopologicalSpace Y] + [IsTopologicalAddGroup Y] [CompactSpace Y] [TotallyDisconnectedSpace Y] + hom_type (X →ₜ+ Y) from (ProfiniteAddGrp.of X) to (ProfiniteAddGrp.of Y) namespace ProfiniteGrp @@ -139,18 +108,11 @@ namespace ProfiniteGrp instance {M N : ProfiniteGrp.{u}} : CoeFun (M ⟶ N) (fun _ ↦ M → N) where coe f := f.hom -@[to_additive (attr := simp)] -lemma hom_id {A : ProfiniteGrp.{u}} : (𝟙 A : A ⟶ A).hom = ContinuousMonoidHom.id A := rfl - /- Provided for rewriting. -/ @[to_additive] lemma id_apply (A : ProfiniteGrp.{u}) (a : A) : (𝟙 A : A ⟶ A) a = a := by simp -@[to_additive (attr := simp)] -lemma hom_comp {A B C : ProfiniteGrp.{u}} (f : A ⟶ B) (g : B ⟶ C) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - /- Provided for rewriting. -/ @[to_additive] lemma comp_apply {A B C : ProfiniteGrp.{u}} (f : A ⟶ B) (g : B ⟶ C) (a : A) : @@ -166,13 +128,6 @@ variable {X Y Z : Type u} [Group X] [TopologicalSpace X] [IsTopologicalGroup X] [IsTopologicalGroup Y] [CompactSpace Y] [TotallyDisconnectedSpace Y] [Group Z] [TopologicalSpace Z] [IsTopologicalGroup Z] [CompactSpace Z] [TotallyDisconnectedSpace Z] -@[to_additive (attr := simp)] -lemma hom_ofHom (f : X →ₜ* Y) : (ofHom f).hom = f := rfl - -@[to_additive (attr := simp)] -lemma ofHom_hom {A B : ProfiniteGrp.{u}} (f : A ⟶ B) : - ofHom (Hom.hom f) = f := rfl - @[to_additive (attr := simp)] lemma ofHom_id : ofHom (ContinuousMonoidHom.id X) = 𝟙 (of X) := rfl diff --git a/Mathlib/Topology/Category/TopCat/Basic.lean b/Mathlib/Topology/Category/TopCat/Basic.lean index 314d465ed09a31..c8b49a1687540b 100644 --- a/Mathlib/Topology/Category/TopCat/Basic.lean +++ b/Mathlib/Topology/Category/TopCat/Basic.lean @@ -8,6 +8,7 @@ module public import Mathlib.CategoryTheory.ConcreteCategory.Forget public import Mathlib.CategoryTheory.Elementwise public import Mathlib.Topology.ContinuousMap.Basic +public import Mathlib.Tactic.CategoryTheory.MkConcreteCategory /-! # Category instance for topological spaces @@ -63,53 +64,19 @@ lemma coe_of (X : Type u) [TopologicalSpace X] : (of X : Type u) = X := lemma of_carrier (X : TopCat.{u}) : of X = X := rfl -variable {X} in -/-- The type of morphisms in `TopCat`. -/ -@[ext] -structure Hom (X Y : TopCat.{u}) where - --private mk :: - /-- The underlying `ContinuousMap`. -/ - hom' : C(X, Y) - -instance : Category TopCat where - Hom X Y := Hom X Y - id X := ⟨ContinuousMap.id X⟩ - comp f g := ⟨g.hom'.comp f.hom'⟩ - -instance : ConcreteCategory.{u} TopCat (fun X Y => C(X, Y)) where - hom := Hom.hom' - ofHom f := ⟨f⟩ - -/-- Turn a morphism in `TopCat` back into a `ContinuousMap`. -/ -abbrev Hom.hom {X Y : TopCat.{u}} (f : Hom X Y) := - ConcreteCategory.hom (C := TopCat) f - -/-- Typecheck a `ContinuousMap` as a morphism in `TopCat`. -/ -abbrev ofHom {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : of X ⟶ of Y := - ConcreteCategory.ofHom (C := TopCat) f - -/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/ -def Hom.Simps.hom (X Y : TopCat) (f : Hom X Y) := - f.hom - -initialize_simps_projections Hom (hom' → hom) +mk_concrete_category TopCat.{u} C(·, ·) ContinuousMap.id ContinuousMap.comp + with_of_hom {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] + hom_type C(X, Y) from (TopCat.of X) to (TopCat.of Y) /-! The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`. -/ -@[simp] -lemma hom_id {X : TopCat.{u}} : (𝟙 X : X ⟶ X).hom = ContinuousMap.id X := rfl - @[simp] theorem id_app (X : TopCat.{u}) (x : ↑X) : (𝟙 X : X ⟶ X) x = x := rfl @[simp] theorem coe_id (X : TopCat.{u}) : (𝟙 X : X → X) = id := rfl -@[simp] -lemma hom_comp {X Y Z : TopCat.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) : - (f ≫ g).hom = g.hom.comp f.hom := rfl - @[simp] theorem comp_app {X Y Z : TopCat.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g : X → Z) x = g (f x) := rfl @@ -125,14 +92,6 @@ lemma hom_ext {X Y : TopCat.{u}} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g := lemma ext {X Y : TopCat.{u}} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := ConcreteCategory.hom_ext _ _ w -@[simp] -lemma hom_ofHom {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : - (ofHom f).hom = f := rfl - -@[simp] -lemma ofHom_hom {X Y : TopCat.{u}} (f : X ⟶ Y) : - ofHom (Hom.hom f) = f := rfl - @[simp] lemma ofHom_id {X : Type u} [TopologicalSpace X] : ofHom (ContinuousMap.id X) = 𝟙 (of X) := rfl diff --git a/Mathlib/Topology/Category/TopPair.lean b/Mathlib/Topology/Category/TopPair.lean index 0ab7c2198d79c0..b2637bd14f5d58 100644 --- a/Mathlib/Topology/Category/TopPair.lean +++ b/Mathlib/Topology/Category/TopPair.lean @@ -52,7 +52,7 @@ abbrev of {A X : TopCat.{u}} (f : A ⟶ X) (h : Topology.IsEmbedding f) : TopPai /-- Constructor for a topological pair (X, A) where A ⊆ X. -/ abbrev ofSubset {X : TopCat.{u}} (A : Set X) : TopPair.{u} := TopPair.of (A := (TopCat.of A)) - (X := X) ⟨{ toFun := Subtype.val }⟩ Topology.IsEmbedding.subtypeVal + (X := X) (TopCat.ofHom { toFun := Subtype.val }) Topology.IsEmbedding.subtypeVal /-- Constructs the topological pair `(X, ∅)` from `X : TopCat`. -/ abbrev ofTopCat (X : TopCat.{u}) : TopPair.{u} := diff --git a/Mathlib/Topology/Category/UniformSpace.lean b/Mathlib/Topology/Category/UniformSpace.lean index 3cfb33de484fce..4c1e671e933031 100644 --- a/Mathlib/Topology/Category/UniformSpace.lean +++ b/Mathlib/Topology/Category/UniformSpace.lean @@ -42,37 +42,15 @@ namespace UniformSpaceCat instance : CoeSort UniformSpaceCat Type* := ⟨carrier⟩ -/-- A bundled uniform continuous map. -/ -@[ext] -structure Hom (X Y : UniformSpaceCat) where - /-- The underlying `UniformContinuous` function. -/ - hom' : { f : X → Y // UniformContinuous f } - -instance : LargeCategory.{u} UniformSpaceCat.{u} where - Hom := Hom - id X := ⟨id, uniformContinuous_id⟩ - comp f g := ⟨⟨g.hom'.val ∘ f.hom'.val, g.hom'.property.comp f.hom'.property⟩⟩ - id_comp := by intros; apply Hom.ext; simp - comp_id := by intros; apply Hom.ext; simp - assoc := by intros; apply Hom.ext; ext; simp - instance instFunLike (X Y : UniformSpaceCat) : FunLike { f : X → Y // UniformContinuous f } X Y where coe := Subtype.val coe_injective' _ _ h := Subtype.ext h -instance : ConcreteCategory UniformSpaceCat ({ f : · → · // UniformContinuous f }) where - hom f := f.hom' - ofHom f := ⟨f⟩ - -/-- Turn a morphism in `UniformSpaceCat` back into a function which is `UniformContinuous`. -/ -abbrev Hom.hom {X Y : UniformSpaceCat} (f : Hom X Y) := - ConcreteCategory.hom (C := UniformSpaceCat) f - -/-- Typecheck a function which is `UniformContinuous` as a morphism in `UniformSpaceCat`. -/ -abbrev ofHom {X Y : Type u} [UniformSpace X] [UniformSpace Y] - (f : { f : X → Y // UniformContinuous f }) : of X ⟶ of Y := - ConcreteCategory.ofHom f +mk_concrete_category UniformSpaceCat.{u} ({ f : · → · // UniformContinuous f }) + (fun _ ↦ ⟨id, uniformContinuous_id⟩) (fun g f ↦ ⟨g ∘ f, g.property.comp f.property⟩) + with_of_hom {X Y : Type u} [UniformSpace X] [UniformSpace Y] + hom_type { f : X → Y // UniformContinuous f } from (of X) to (of Y) instance : Inhabited UniformSpaceCat := ⟨UniformSpaceCat.of Empty⟩ @@ -80,20 +58,6 @@ instance : Inhabited UniformSpaceCat := theorem coe_of (X : Type u) [UniformSpace X] : (of X : Type u) = X := rfl -@[simp] -theorem hom_comp {X Y Z : UniformSpaceCat} (f : X ⟶ Y) (g : Y ⟶ Z) : - (f ≫ g).hom = ⟨g ∘ f, g.hom.prop.comp f.hom.prop⟩ := - rfl - -@[simp] -theorem hom_id (X : UniformSpaceCat) : (𝟙 X : X ⟶ X).hom = ⟨id, uniformContinuous_id⟩ := - rfl - -@[simp] -theorem hom_ofHom {X Y : Type u} [UniformSpace X] [UniformSpace Y] - (f : { f : X → Y // UniformContinuous f }) : (ofHom f).hom = f := - rfl - theorem coe_comp {X Y Z : UniformSpaceCat} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g : X → Z) = g ∘ f := rfl @@ -101,7 +65,7 @@ theorem coe_id (X : UniformSpaceCat) : (𝟙 X : X → X) = id := rfl theorem coe_mk {X Y : UniformSpaceCat} (f : X → Y) (hf : UniformContinuous f) : - (⟨f, hf⟩ : X ⟶ Y).hom = f := + ((ofHom ⟨f, hf⟩ : X ⟶ Y).hom : X → Y) = f := rfl @[ext] @@ -206,9 +170,8 @@ noncomputable def completionFunctor : UniformSpaceCat ⥤ CpltSepUniformSpace wh /-- The inclusion of a uniform space into its completion. -/ noncomputable def completionHom (X : UniformSpaceCat) : - X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj (completionFunctor.obj X) where - hom'.val := ((↑) : X → Completion X) - hom'.property := Completion.uniformContinuous_coe X + X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj (completionFunctor.obj X) := + ofHom ⟨((↑) : X → Completion X), Completion.uniformContinuous_coe X⟩ @[simp] theorem completionHom_val (X : UniformSpaceCat) (x) : (completionHom X) x = (x : Completion X) := diff --git a/Mathlib/Topology/Sheaves/LocalPredicate.lean b/Mathlib/Topology/Sheaves/LocalPredicate.lean index ce9ba2712e09b1..3b5f28bb6a914b 100644 --- a/Mathlib/Topology/Sheaves/LocalPredicate.lean +++ b/Mathlib/Topology/Sheaves/LocalPredicate.lean @@ -361,8 +361,8 @@ the presheaf of continuous functions. def subpresheafContinuousPrelocalIsoPresheafToTop {X : TopCat.{u}} (T : TopCat.{u}) : subpresheafToTypes (continuousPrelocal X T) ≅ presheafToTop X T := NatIso.ofComponents fun X ↦ - { hom := ↾(by rintro ⟨f, c⟩; exact ofHom ⟨f, c⟩) - inv := ↾(by rintro ⟨f, c⟩; exact ⟨f, c⟩) } + { hom := ↾fun f ↦ ofHom ⟨f.1, f.2⟩ + inv := ↾fun f ↦ ⟨f.1, f.1.2⟩ } /-- The sheaf of continuous functions on `X` with values in a space `T`. -/ diff --git a/MathlibTest/CategoryTheory/MkConcreteCategory.lean b/MathlibTest/CategoryTheory/MkConcreteCategory.lean new file mode 100644 index 00000000000000..ed56500b4be18a --- /dev/null +++ b/MathlibTest/CategoryTheory/MkConcreteCategory.lean @@ -0,0 +1,434 @@ +/- +Copyright (c) 2026 Dagur Asgeirsson. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Dagur Asgeirsson +-/ +module + +import Mathlib.Tactic.CategoryTheory.MkConcreteCategory +public import Mathlib.Algebra.Module.LinearMap.Defs +public import Mathlib.CategoryTheory.ConcreteCategory.Basic + +open CategoryTheory + +universe v u + +structure TestCat where + α : Type u + +namespace TestCat + +@[ext] +structure Fun (X Y : TestCat.{u}) where + toFun : X.α → Y.α + +instance (X Y : TestCat.{u}) : FunLike (Fun X Y) X.α Y.α where + coe := Fun.toFun + coe_injective' _ _ _ := by aesop + +protected def Fun.id (X : TestCat.{u}) : Fun X X where + toFun := id + +protected def Fun.comp {X Y Z : TestCat.{u}} (g : Fun Y Z) (f : Fun X Y) : Fun X Z where + toFun := g.toFun ∘ f.toFun + +mk_concrete_category TestCat Fun Fun.id Fun.comp + +/-- info: TestCat.Hom.{u_1} (X Y : TestCat) : Type u_1 -/ +#guard_msgs in +#check Hom + +/-- info: TestCat.Hom.mk.{u_1} {X Y : TestCat} (hom' : X.Fun Y) : X.Hom Y -/ +#guard_msgs in +#check Hom.mk + +/-- info: TestCat.Hom.hom'.{u_1} {X Y : TestCat} (self : X.Hom Y) : X.Fun Y -/ +#guard_msgs in +#check Hom.hom' + +/-- info: TestCat.Hom.ext.{u_1} {X Y : TestCat} {x y : X.Hom Y} (hom' : x.hom' = y.hom') : x = y -/ +#guard_msgs in +#check Hom.ext + +/-- info: TestCat.instCategory.{u_1} : Category.{u_1, u_1 + 1} TestCat -/ +#guard_msgs in +#check TestCat.instCategory + +/-- info: TestCat.instConcreteCategory.{u_1} : ConcreteCategory TestCat Fun -/ +#guard_msgs in +#check TestCat.instConcreteCategory + +/-- info: TestCat.Hom.hom.{u_1} {X Y : TestCat} (f : X ⟶ Y) : X.Fun Y -/ +#guard_msgs in +#check Hom.hom + +/-- info: TestCat.ofHom.{u_1} {X Y : TestCat} (f : X.Fun Y) : X ⟶ Y -/ +#guard_msgs in +#check ofHom + + +/-- info: TestCat.hom_id.{u_1} {X : TestCat} : Hom.hom (𝟙 X) = Fun.id X -/ +#guard_msgs in +#check hom_id + +/-- +info: TestCat.hom_comp.{u_1} {X Y Z : TestCat} (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f) +-/ +#guard_msgs in +#check hom_comp + +/-- info: TestCat.hom_ofHom.{u_1} {X Y : TestCat} (f : X.Fun Y) : Hom.hom (ConcreteCategory.ofHom f) = f -/ +#guard_msgs in +#check hom_ofHom + +/-- info: TestCat.ofHom_hom.{u_1} {X Y : TestCat} (f : X ⟶ Y) : ConcreteCategory.ofHom (Hom.hom f) = f -/ +#guard_msgs in +#check ofHom_hom + +example : Category TestCat := inferInstance + +example : ConcreteCategory TestCat Fun := inferInstance + +example {X Y : TestCat} (f : X ⟶ Y) : f.hom = ConcreteCategory.hom f := rfl + +example {X Y : TestCat} (f : Fun X Y) : (ofHom f).hom = f := by + dsimp + +example {X Y : TestCat} (f : X ⟶ Y) : ofHom f.hom = f := by + dsimp + +example {X : TestCat} : (𝟙 X : X ⟶ X).hom = Fun.id X := by + dsimp + +example {X Y Z : TestCat} (f : X ⟶ Y) (g : Y ⟶ Z) : + Hom.hom (f ≫ g) = Fun.comp g.hom f.hom := by + dsimp + +example {X Y : TestCat} (f g : X ⟶ Y) (h : f.hom = g.hom) : f = g := + Hom.ext h + +example {X Y : TestCat} (f g : X ⟶ Y) (h : ∀ x, f x = g x) : f = g := by + cat_disch + +example {X Y : TestCat} (f : Fun X Y) (x : X.α) : ofHom f x = f x := by + simp + +@[simps! hom] +def morphism (X : TestCat) : X ⟶ X := ofHom ⟨id⟩ + +/-- info: TestCat.morphism_hom.{u_1} (X : TestCat) : Hom.hom X.morphism = { toFun := id } -/ +#guard_msgs in +#check morphism_hom + +end TestCat + +variable (R : Type u) [Ring R] + +structure ModuleTestCat where + carrier : Type v + [isAddCommGroup : AddCommGroup carrier] + [isModule : Module R carrier] + +attribute [instance] ModuleTestCat.isAddCommGroup +attribute [instance 1100] ModuleTestCat.isModule + +namespace ModuleTestCat + +abbrev of (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] : + ModuleTestCat R := + ⟨M⟩ + +instance : CoeSort (ModuleTestCat.{v} R) (Type v) := + ⟨ModuleTestCat.carrier⟩ + +attribute [coe] ModuleTestCat.carrier + +variable {R} in +mk_concrete_category (ModuleTestCat.{v} R) (· →ₗ[R] ·) (@LinearMap.id R ·) LinearMap.comp + with_of_hom {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] + hom_type (X →ₗ[R] Y) from (of R X) to (of R Y) + +/-- info: ModuleTestCat.Hom.{v, u} {R : Type u} [Ring R] (X Y : ModuleTestCat R) : Type v -/ +#guard_msgs in +#check Hom + +/-- +info: ModuleTestCat.Hom.mk.{v, u} {R : Type u} [Ring R] {X Y : ModuleTestCat R} (hom' : ↑X →ₗ[R] ↑Y) : X.Hom Y +-/ +#guard_msgs in +#check Hom.mk + +/-- +info: ModuleTestCat.Hom.hom'.{v, u} {R : Type u} [Ring R] {X Y : ModuleTestCat R} (self : X.Hom Y) : ↑X →ₗ[R] ↑Y +-/ +#guard_msgs in +#check Hom.hom' + +/-- +info: ModuleTestCat.Hom.ext.{v, u} {R : Type u} {inst✝ : Ring R} {X Y : ModuleTestCat R} {x y : X.Hom Y} + (hom' : x.hom' = y.hom') : x = y +-/ +#guard_msgs in +#check Hom.ext + +/-- +info: ModuleTestCat.instCategory.{v, u} {R : Type u} [Ring R] : Category.{v, max (v + 1) u} (ModuleTestCat R) +-/ +#guard_msgs in +#check ModuleTestCat.instCategory + +/-- +info: ModuleTestCat.instConcreteCategory.{v, u} {R : Type u} [Ring R] : + ConcreteCategory (ModuleTestCat R) fun x1 x2 => ↑x1 →ₗ[R] ↑x2 +-/ +#guard_msgs in +#check ModuleTestCat.instConcreteCategory + +/-- +info: ModuleTestCat.Hom.hom.{v, u} {R : Type u} [Ring R] {X Y : ModuleTestCat R} (f : X ⟶ Y) : ↑X →ₗ[R] ↑Y +-/ +#guard_msgs in +#check Hom.hom + +/-- info: ModuleTestCat.ofHom.{v, u} {R : Type u} [Ring R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] + [Module R Y] (f : X →ₗ[R] Y) : of R X ⟶ of R Y -/ +#guard_msgs in +#check ofHom + + +/-- +info: ModuleTestCat.hom_id.{v, u} {R : Type u} [Ring R] {X : ModuleTestCat R} : Hom.hom (𝟙 X) = LinearMap.id +-/ +#guard_msgs in +#check hom_id + +/-- +info: ModuleTestCat.hom_comp.{v, u} {R : Type u} [Ring R] {X Y Z : ModuleTestCat R} (f : X ⟶ Y) (g : Y ⟶ Z) : + Hom.hom (f ≫ g) = Hom.hom g ∘ₗ Hom.hom f +-/ +#guard_msgs in +#check hom_comp + +/-- +info: ModuleTestCat.hom_ofHom.{v, u} {R : Type u} [Ring R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] + [Module R Y] (f : X →ₗ[R] Y) : Hom.hom (ofHom f) = f +-/ +#guard_msgs in +#check hom_ofHom + +/-- +info: ModuleTestCat.ofHom_hom.{v, u} {R : Type u} [Ring R] {X Y : ModuleTestCat R} (f : X ⟶ Y) : + ConcreteCategory.ofHom (Hom.hom f) = f +-/ +#guard_msgs in +#check ofHom_hom + +example : Category (ModuleTestCat.{v} R) := inferInstance + +example : ConcreteCategory (ModuleTestCat.{v} R) (fun X Y => X →ₗ[R] Y) := inferInstance + +example {X Y : ModuleTestCat.{v} R} (f : X ⟶ Y) : f.hom = ConcreteCategory.hom f := rfl + +example {X Y : ModuleTestCat.{v} R} (f : X →ₗ[R] Y) : (ofHom f).hom = f := by + dsimp + +example {X Y : ModuleTestCat.{v} R} (f : X ⟶ Y) : ofHom f.hom = f := by + dsimp + +example {X : ModuleTestCat.{v} R} : (𝟙 X : X ⟶ X).hom = LinearMap.id := by + dsimp + +example {X Y Z : ModuleTestCat.{v} R} (f : X ⟶ Y) (g : Y ⟶ Z) : + Hom.hom (f ≫ g) = LinearMap.comp g.hom f.hom := by + dsimp + +example {X Y : ModuleTestCat.{v} R} (f g : X ⟶ Y) (h : f.hom = g.hom) : f = g := + Hom.ext h + +example {X Y : ModuleTestCat.{v} R} (f g : X ⟶ Y) (h : ∀ x, f x = g x) : f = g := by + cat_disch + +example {X Y : ModuleTestCat.{v} R} (f : X →ₗ[R] Y) (x : X) : ofHom f x = f x := by + simp + +@[simps! hom] +def morphism (X : ModuleTestCat.{v} R) : X ⟶ X := ofHom (LinearMap.id) + +/-- +info: ModuleTestCat.morphism_hom.{v, u} (R : Type u) [Ring R] (X : ModuleTestCat R) : Hom.hom (morphism R X) = LinearMap.id +-/ +#guard_msgs in +#check morphism_hom + +end ModuleTestCat + +structure AdditiveTestCat where + carrier : Type u + [str : AddMonoid carrier] + +@[to_additive AdditiveTestCat] +structure MultiplicativeTestCat where + carrier : Type u + [str : Monoid carrier] + +attribute [instance] AdditiveTestCat.str MultiplicativeTestCat.str + +namespace MultiplicativeTestCat + +@[to_additive] +abbrev of (M : Type u) [Monoid M] : MultiplicativeTestCat := + ⟨M⟩ + +@[to_additive instCoeSortAdditiveTestCat] +instance instCoeSort : CoeSort MultiplicativeTestCat (Type u) := + ⟨MultiplicativeTestCat.carrier⟩ + +end MultiplicativeTestCat + +attribute [coe] AdditiveTestCat.carrier MultiplicativeTestCat.carrier + +@[to_additive AdditiveTestCat] +mk_concrete_category MultiplicativeTestCat.{u} (· →* ·) MonoidHom.id MonoidHom.comp + with_of_hom {X Y : Type u} [Monoid X] [Monoid Y] + hom_type (X →* Y) from (MultiplicativeTestCat.of X) to (MultiplicativeTestCat.of Y) + to_additive AdditiveTestCat.{u} (· →+ ·) AddMonoidHom.id AddMonoidHom.comp + with_of_hom {X Y : Type u} [AddMonoid X] [AddMonoid Y] + hom_type (X →+ Y) from (AdditiveTestCat.of X) to (AdditiveTestCat.of Y) + +namespace MultiplicativeTestCat + +/-- info: MultiplicativeTestCat.Hom.{u} (X Y : MultiplicativeTestCat) : Type u -/ +#guard_msgs in +#check Hom + +/-- info: MultiplicativeTestCat.instCategory.{u} : Category.{u, u + 1} MultiplicativeTestCat -/ +#guard_msgs in +#check MultiplicativeTestCat.instCategory + +/-- +info: MultiplicativeTestCat.instConcreteCategory.{u} : ConcreteCategory MultiplicativeTestCat fun x1 x2 => ↑x1 →* ↑x2 +-/ +#guard_msgs in +#check MultiplicativeTestCat.instConcreteCategory + +/-- info: MultiplicativeTestCat.Hom.hom.{u} {X Y : MultiplicativeTestCat} (f : X ⟶ Y) : ↑X →* ↑Y -/ +#guard_msgs in +#check Hom.hom + +/-- info: MultiplicativeTestCat.ofHom.{u} {X Y : Type u} [Monoid X] [Monoid Y] (f : X →* Y) : of X ⟶ of Y -/ +#guard_msgs in +#check ofHom + +/-- +info: MultiplicativeTestCat.hom_id.{u} {X : MultiplicativeTestCat} : Hom.hom (𝟙 X) = MonoidHom.id ↑X +-/ +#guard_msgs in +#check hom_id + +/-- +info: MultiplicativeTestCat.hom_comp.{u} {X Y Z : MultiplicativeTestCat} (f : X ⟶ Y) (g : Y ⟶ Z) : + Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f) +-/ +#guard_msgs in +#check hom_comp + +/-- +info: MultiplicativeTestCat.hom_ofHom.{u} {X Y : Type u} [Monoid X] [Monoid Y] (f : X →* Y) : Hom.hom (ofHom f) = f +-/ +#guard_msgs in +#check hom_ofHom + +/-- +info: MultiplicativeTestCat.ofHom_hom.{u} {X Y : MultiplicativeTestCat} (f : X ⟶ Y) : ConcreteCategory.ofHom (Hom.hom f) = f +-/ +#guard_msgs in +#check ofHom_hom + +example : Category MultiplicativeTestCat := inferInstance + +example : ConcreteCategory MultiplicativeTestCat (fun X Y => X →* Y) := inferInstance + +example {X Y : Type u} [Monoid X] [Monoid Y] (f : X →* Y) : (ofHom f).hom = f := by + dsimp + +example {X Y Z : MultiplicativeTestCat} (f : X ⟶ Y) (g : Y ⟶ Z) : + Hom.hom (f ≫ g) = MonoidHom.comp g.hom f.hom := by + dsimp + +@[simps! hom] +def morphism (X : MultiplicativeTestCat) : X ⟶ X := ofHom (MonoidHom.id _) + +/-- +info: MultiplicativeTestCat.morphism_hom.{u_1} (X : MultiplicativeTestCat) : Hom.hom X.morphism = MonoidHom.id ↑X +-/ +#guard_msgs in +#check morphism_hom + +end MultiplicativeTestCat + +namespace AdditiveTestCat + +/-- info: AdditiveTestCat.Hom.{u} (X Y : AdditiveTestCat) : Type u -/ +#guard_msgs in +#check Hom + +/-- info: AdditiveTestCat.instCategory.{u} : Category.{u, u + 1} AdditiveTestCat -/ +#guard_msgs in +#check AdditiveTestCat.instCategory + +/-- +info: AdditiveTestCat.instConcreteCategory.{u} : ConcreteCategory AdditiveTestCat fun x1 x2 => ↑x1 →+ ↑x2 +-/ +#guard_msgs in +#check AdditiveTestCat.instConcreteCategory + +/-- info: AdditiveTestCat.Hom.hom.{u} {X Y : AdditiveTestCat} (f : X ⟶ Y) : ↑X →+ ↑Y -/ +#guard_msgs in +#check Hom.hom + +/-- info: AdditiveTestCat.ofHom.{u} {X Y : Type u} [AddMonoid X] [AddMonoid Y] (f : X →+ Y) : of X ⟶ of Y -/ +#guard_msgs in +#check ofHom + +/-- info: AdditiveTestCat.hom_id.{u} {X : AdditiveTestCat} : Hom.hom (𝟙 X) = AddMonoidHom.id ↑X -/ +#guard_msgs in +#check hom_id + +/-- +info: AdditiveTestCat.hom_comp.{u} {X Y Z : AdditiveTestCat} (f : X ⟶ Y) (g : Y ⟶ Z) : + Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f) +-/ +#guard_msgs in +#check hom_comp + +/-- info: AdditiveTestCat.hom_ofHom.{u} {X Y : Type u} [AddMonoid X] [AddMonoid Y] (f : X →+ Y) : Hom.hom (ofHom f) = f -/ +#guard_msgs in +#check hom_ofHom + +/-- +info: AdditiveTestCat.ofHom_hom.{u} {X Y : AdditiveTestCat} (f : X ⟶ Y) : ConcreteCategory.ofHom (Hom.hom f) = f +-/ +#guard_msgs in +#check ofHom_hom + +example : Category AdditiveTestCat := inferInstance + +example : ConcreteCategory AdditiveTestCat (fun X Y => X →+ Y) := inferInstance + +example {X Y : Type u} [AddMonoid X] [AddMonoid Y] (f : X →+ Y) : (ofHom f).hom = f := by + dsimp + +example {X Y Z : AdditiveTestCat} (f : X ⟶ Y) (g : Y ⟶ Z) : + Hom.hom (f ≫ g) = AddMonoidHom.comp g.hom f.hom := by + dsimp + +@[simps! hom] +def morphism (X : AdditiveTestCat) : X ⟶ X := ofHom (AddMonoidHom.id _) + +/-- +info: AdditiveTestCat.morphism_hom.{u_1} (X : AdditiveTestCat) : Hom.hom X.morphism = AddMonoidHom.id ↑X +-/ +#guard_msgs in +#check morphism_hom + +end AdditiveTestCat