chore(CategoryTheory): start using mk_concrete_category

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

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
 

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 _
 

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]

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]