refactor(category_theory/endomorphism): move to a dedicated file; pro…

…ve simple lemmas (#1195)

* Move definitions of `End` and `Aut` to a dedicated file

* Adjust some proofs, use `namespace`, add docstrings

* `functor.map` and `functor.map_iso` define homomorphisms of `End/Aut`

* Define `functor.map_End` and `functor.map_Aut`

src/category/fold.lean

@@ -45,7 +45,7 @@ import tactic.squeeze
 import algebra.group algebra.opposites
 import data.list.basic
 import category.traversable.instances category.traversable.lemmas
-import category_theory.category category_theory.types category_theory.instances.kleisli
+import category_theory.category category_theory.endomorphism category_theory.types category_theory.instances.kleisli
 import category.applicative
 
 universes u v

src/category_theory/category.lean

@@ -125,23 +125,6 @@ instance ulift_category : category.{v} (ulift.{u'} C) :=
 example (D : Type u) [small_category D] : large_category (ulift.{u+1} D) := by apply_instance
 end
 
-section
-variables {C : Type u}
-
-def End [has_hom.{v} C] (X : C) := X ⟶ X
-
-instance End.has_one [category_struct.{v+1} C] {X : C} : has_one (End X) := by refine { one := 𝟙 X }
-/-- Multiplication of endomorphisms agrees with `function.comp`, not `category_struct.comp`. -/
-instance End.has_mul [category_struct.{v+1} C] {X : C} : has_mul (End X) := by refine { mul := λ x y, y ≫ x }
-instance End.monoid [category.{v+1} C] {X : C} : monoid (End X) :=
-by refine { .. End.has_one, .. End.has_mul, .. }; dsimp [has_mul.mul,has_one.one]; obviously
-
-@[simp] lemma End.one_def {C : Type u} [category_struct.{v+1} C] {X : C} : (1 : End X) = 𝟙 X := rfl
-
-@[simp] lemma End.mul_def {C : Type u} [category_struct.{v+1} C] {X : C} (xs ys : End X) : xs * ys = ys ≫ xs := rfl
-
-end
-
 end category_theory
 
 open category_theory

src/category_theory/endomorphism.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2019 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov, Scott Morrison, Simon Hudon
+
+Definition and basic properties of endomorphisms and automorphisms of an object in a category.
+-/
+
+import category_theory.category category_theory.isomorphism category_theory.groupoid category_theory.functor
+import algebra.group.units data.equiv.algebra
+
+universes v v' u u'
+
+namespace category_theory
+
+/-- Endomorphisms of an object in a category. Arguments order in multiplication agrees with `function.comp`, not with `category.comp`. -/
+def End {C : Type u} [𝒞_struct : category_struct.{v+1} C] (X : C) := X ⟶ X
+
+namespace End
+
+section struct
+
+variables {C : Type u} [𝒞_struct : category_struct.{v+1} C] (X : C)
+include 𝒞_struct
+
+instance has_one : has_one (End X) := ⟨𝟙 X⟩
+
+/-- Multiplication of endomorphisms agrees with `function.comp`, not `category_struct.comp`. -/
+instance has_mul : has_mul (End X) := ⟨λ x y, y ≫ x⟩
+
+variable {X}
+
+@[simp] lemma one_def : (1 : End X) = 𝟙 X := rfl
+
+@[simp] lemma mul_def (xs ys : End X) : xs * ys = ys ≫ xs := rfl
+
+end struct
+
+/-- Endomorphisms of an object form a monoid -/
+instance monoid {C : Type u} [category.{v+1} C] {X : C} : monoid (End X) :=
+{ mul_one := category.id_comp C,
+  one_mul := category.comp_id C,
+  mul_assoc := λ x y z, (category.assoc C z y x).symm,
+  ..End.has_mul X, ..End.has_one X }
+
+/-- In a groupoid, endomorphisms form a group -/
+instance group {C : Type u} [groupoid.{v+1} C] (X : C) : group (End X) :=
+{ mul_left_inv := groupoid.comp_inv C, inv := groupoid.inv, ..End.monoid }
+
+end End
+
+def Aut {C : Type u} [𝒞 : category.{v+1} C] (X : C) := X ≅ X
+
+attribute [extensionality Aut] iso.ext
+
+namespace Aut
+
+variables {C : Type u} [𝒞 : category.{v+1} C] (X : C)
+include 𝒞
+
+instance: group (Aut X) :=
+by refine { one := iso.refl X,
+            inv := iso.symm,
+            mul := flip iso.trans, .. } ; dunfold flip; obviously
+
+def units_End_eqv_Aut : (units (End X)) ≃* Aut X :=
+{ to_fun := λ f, ⟨f.1, f.2, f.4, f.3⟩,
+  inv_fun := λ f, ⟨f.1, f.2, f.4, f.3⟩,
+  left_inv := λ ⟨f₁, f₂, f₃, f₄⟩, rfl,
+  right_inv := λ ⟨f₁, f₂, f₃, f₄⟩, rfl,
+  hom := ⟨λ f g, by rcases f; rcases g; refl⟩ }
+
+end Aut
+
+namespace functor
+
+variables {C : Type u} [𝒞 : category.{v+1} C] {D : Type u'} [𝒟 : category.{v'+1} D] (f : C ⥤ D) {X : C}
+include 𝒞 𝒟
+
+def map_End : End X → End (f.obj X) := functor.map f
+
+instance map_End.is_monoid_hom : is_monoid_hom (f.map_End : End X → End (f.obj X)) :=
+{ map_mul := λ x y, f.map_comp y x,
+  map_one := f.map_id X }
+
+def map_Aut : Aut X → Aut (f.obj X) := functor.map_iso f
+
+instance map_Aut.is_group_hom : is_group_hom (f.map_Aut : Aut X → Aut (f.obj X)) :=
+{ map_mul := λ x y, f.map_iso_trans y x }
+
+end functor
+
+instance functor.map_End_is_group_hom {C : Type u} [𝒞 : groupoid.{v+1} C]
+                                      {D : Type u'} [𝒟 : groupoid.{v'+1} D] (f : C ⥤ D) {X : C} :
+  is_group_hom (f.map_End : End X → End (f.obj X)) :=
+{ ..functor.map_End.is_monoid_hom f }
+
+end category_theory

src/category_theory/isomorphism.lean

@@ -212,6 +212,10 @@ def map_iso (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : F.obj X ≅ F.obj Y :=
 @[simp] lemma map_iso_hom (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : (F.map_iso i).hom = F.map i.hom := rfl
 @[simp] lemma map_iso_inv (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : (F.map_iso i).inv = F.map i.inv := rfl
 
+@[simp] lemma map_iso_trans (F : C ⥤ D) {X Y Z : C} (i : X ≅ Y) (j : Y ≅ Z) :
+  F.map_iso (i ≪≫ j) = (F.map_iso i) ≪≫ (F.map_iso j) :=
+by ext; apply functor.map_comp
+
 instance (F : C ⥤ D) (f : X ⟶ Y) [is_iso f] : is_iso (F.map f) :=
 { ..(F.map_iso (as_iso f)) }
 
@@ -228,18 +232,3 @@ by rw [←map_comp, is_iso.inv_hom_id, map_id]
 end functor
 
 end category_theory
-
-namespace category_theory
-
-variables {C : Type u} [𝒞 : category.{v+1} C]
-include 𝒞
-
-def Aut (X : C) := X ≅ X
-
-attribute [extensionality Aut] iso.ext
-
-instance {X : C} : group (Aut X) :=
-by refine { one := iso.refl X,
-            inv := iso.symm,
-            mul := flip iso.trans, .. } ; dunfold flip; obviously
-end category_theory