feat(category_theory/commas): add simp-lemmas for comma categories (#503

)

category_theory/comma.lean

@@ -1,10 +1,11 @@
 -- Copyright (c) 2018 Scott Morrison. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
--- Authors: Scott Morrison
+-- Authors: Scott Morrison, Johan Commelin
 
 import category_theory.types
 import category_theory.isomorphism
 import category_theory.whiskering
+import category_theory.opposites
 
 namespace category_theory
 
@@ -60,6 +61,14 @@ instance comma_category : category (comma L R) :=
 
 namespace comma
 
+section
+variables {X Y Z : comma L R} {f : X ⟶ Y} {g : Y ⟶ Z}
+
+@[simp] lemma comp_left  : (f ≫ g).left  = f.left ≫ g.left   := rfl
+@[simp] lemma comp_right : (f ≫ g).right = f.right ≫ g.right := rfl
+
+end
+
 variables (L) (R)
 
 def fst : comma L R ⥤ A :=
@@ -78,8 +87,8 @@ def snd : comma L R ⥤ B :=
 def nat_trans : fst L R ⋙ L ⟹ snd L R ⋙ R :=
 { app := λ X, X.hom }
 
-variables {L₁ : A ⥤ T} {L₂ : A ⥤ T}
-variables {R₁ : B ⥤ T} {R₂ : B ⥤ T}
+section
+variables {L₁ L₂ L₃ : A ⥤ T} {R₁ R₂ R₃ : B ⥤ T}
 
 def map_left (l : L₁ ⟹ L₂) : comma L₂ R ⥤ comma L₁ R :=
 { obj := λ X,
@@ -91,6 +100,44 @@ def map_left (l : L₁ ⟹ L₂) : comma L₂ R ⥤ comma L₁ R :=
     right := f.right,
     w' := by tidy; rw [←category.assoc, l.naturality f.left, category.assoc]; tidy } }
 
+section
+variables {X Y : comma L₂ R} {f : X ⟶ Y} {l : L₁ ⟹ L₂}
+@[simp] lemma map_left_obj_left  : ((map_left R l).obj X).left  = X.left                := rfl
+@[simp] lemma map_left_obj_right : ((map_left R l).obj X).right = X.right               := rfl
+@[simp] lemma map_left_obj_hom   : ((map_left R l).obj X).hom   = l.app X.left ≫ X.hom := rfl
+@[simp] lemma map_left_map_left  : ((map_left R l).map f).left  = f.left                := rfl
+@[simp] lemma map_left_map_right : ((map_left R l).map f).right = f.right               := rfl
+end
+
+def map_left_id : map_left R (𝟙 L) ≅ functor.id _ :=
+{ hom :=
+  { app := λ X, { left := 𝟙 _, right := 𝟙 _ } },
+  inv :=
+  { app := λ X, { left := 𝟙 _, right := 𝟙 _ } } }
+
+section
+variables {X : comma L R}
+@[simp] lemma map_left_id_hom_app_left  : (((map_left_id L R).hom).app X).left  = 𝟙 (X.left)  := rfl
+@[simp] lemma map_left_id_hom_app_right : (((map_left_id L R).hom).app X).right = 𝟙 (X.right) := rfl
+@[simp] lemma map_left_id_inv_app_left  : (((map_left_id L R).inv).app X).left  = 𝟙 (X.left)  := rfl
+@[simp] lemma map_left_id_inv_app_right : (((map_left_id L R).inv).app X).right = 𝟙 (X.right) := rfl
+end
+
+def map_left_comp (l : L₁ ⟹ L₂) (l' : L₂ ⟹ L₃) :
+(map_left R (l ⊟ l')) ≅ (map_left R l') ⋙ (map_left R l) :=
+{ hom :=
+  { app := λ X, { left := 𝟙 _, right := 𝟙 _ } },
+  inv :=
+  { app := λ X, { left := 𝟙 _, right := 𝟙 _ } } }
+
+section
+variables {X : comma L₃ R} {l : L₁ ⟹ L₂} {l' : L₂ ⟹ L₃}
+@[simp] lemma map_left_comp_hom_app_left  : (((map_left_comp R l l').hom).app X).left  = 𝟙 (X.left)  := rfl
+@[simp] lemma map_left_comp_hom_app_right : (((map_left_comp R l l').hom).app X).right = 𝟙 (X.right) := rfl
+@[simp] lemma map_left_comp_inv_app_left  : (((map_left_comp R l l').inv).app X).left  = 𝟙 (X.left)  := rfl
+@[simp] lemma map_left_comp_inv_app_right : (((map_left_comp R l l').inv).app X).right = 𝟙 (X.right) := rfl
+end
+
 def map_right (r : R₁ ⟹ R₂) : comma L R₁ ⥤ comma L R₂ :=
 { obj := λ X,
   { left  := X.left,
@@ -101,6 +148,45 @@ def map_right (r : R₁ ⟹ R₂) : comma L R₁ ⥤ comma L R₂ :=
     right := f.right,
     w' := by tidy; rw [←r.naturality f.right, ←category.assoc]; tidy } }
 
+section
+variables {X Y : comma L R₁} {f : X ⟶ Y} {r : R₁ ⟹ R₂}
+@[simp] lemma map_right_obj_left  : ((map_right L r).obj X).left  = X.left                 := rfl
+@[simp] lemma map_right_obj_right : ((map_right L r).obj X).right = X.right                := rfl
+@[simp] lemma map_right_obj_hom   : ((map_right L r).obj X).hom   = X.hom ≫ r.app X.right := rfl
+@[simp] lemma map_right_map_left  : ((map_right L r).map f).left  = f.left                 := rfl
+@[simp] lemma map_right_map_right : ((map_right L r).map f).right = f.right                := rfl
+end
+
+def map_right_id : map_right L (𝟙 R) ≅ functor.id _ :=
+{ hom :=
+  { app := λ X, { left := 𝟙 _, right := 𝟙 _ } },
+  inv :=
+  { app := λ X, { left := 𝟙 _, right := 𝟙 _ } } }
+
+section
+variables {X : comma L R}
+@[simp] lemma map_right_id_hom_app_left  : (((map_right_id L R).hom).app X).left  = 𝟙 (X.left)  := rfl
+@[simp] lemma map_right_id_hom_app_right : (((map_right_id L R).hom).app X).right = 𝟙 (X.right) := rfl
+@[simp] lemma map_right_id_inv_app_left  : (((map_right_id L R).inv).app X).left  = 𝟙 (X.left)  := rfl
+@[simp] lemma map_right_id_inv_app_right : (((map_right_id L R).inv).app X).right = 𝟙 (X.right) := rfl
+end
+
+def map_right_comp (r : R₁ ⟹ R₂) (r' : R₂ ⟹ R₃) : (map_right L (r ⊟ r')) ≅ (map_right L r) ⋙ (map_right L r') :=
+{ hom :=
+  { app := λ X, { left := 𝟙 _, right := 𝟙 _ } },
+  inv :=
+  { app := λ X, { left := 𝟙 _, right := 𝟙 _ } } }
+
+section
+variables {X : comma L R₁} {r : R₁ ⟹ R₂} {r' : R₂ ⟹ R₃}
+@[simp] lemma map_right_comp_hom_app_left  : (((map_right_comp L r r').hom).app X).left  = 𝟙 (X.left)  := rfl
+@[simp] lemma map_right_comp_hom_app_right : (((map_right_comp L r r').hom).app X).right = 𝟙 (X.right) := rfl
+@[simp] lemma map_right_comp_inv_app_left  : (((map_right_comp L r r').inv).app X).left  = 𝟙 (X.left)  := rfl
+@[simp] lemma map_right_comp_inv_app_right : (((map_right_comp L r r').inv).app X).right = 𝟙 (X.right) := rfl
+end
+
+end
+
 end comma
 
 end category_theory