feat(category_theory): images (#2100)

* feat(category_theory): images

* oops, forgot to add file

* Update src/category_theory/category/default.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* some improvements

* linting

* oops

* Update src/category_theory/limits/shapes/images.lean

Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: 3 people

src/category_theory/category/default.lean

@@ -110,10 +110,59 @@ class epi  (f : X ⟶ Y) : Prop :=
 class mono (f : X ⟶ Y) : Prop :=
 (right_cancellation : Π {Z : C} (g h : Z ⟶ X) (w : g ≫ f = h ≫ f), g = h)
 
-@[simp] lemma cancel_epi  (f : X ⟶ Y) [epi f]  {g h : Y ⟶ Z} : (f ≫ g = f ≫ h) ↔ g = h :=
+instance (X : C) : epi.{v} (𝟙 X) :=
+⟨λ Z g h w, by simpa using w⟩
+instance (X : C) : mono.{v} (𝟙 X) :=
+⟨λ Z g h w, by simpa using w⟩
+
+lemma cancel_epi (f : X ⟶ Y) [epi f]  {g h : Y ⟶ Z} : (f ≫ g = f ≫ h) ↔ g = h :=
 ⟨ λ p, epi.left_cancellation g h p, begin intro a, subst a end ⟩
-@[simp] lemma cancel_mono (f : X ⟶ Y) [mono f] {g h : Z ⟶ X} : (g ≫ f = h ≫ f) ↔ g = h :=
+lemma cancel_mono (f : X ⟶ Y) [mono f] {g h : Z ⟶ X} : (g ≫ f = h ≫ f) ↔ g = h :=
 ⟨ λ p, mono.right_cancellation g h p, begin intro a, subst a end ⟩
+
+lemma cancel_epi_id (f : X ⟶ Y) [epi f] {h : Y ⟶ Y} : (f ≫ h = f) ↔ h = 𝟙 Y :=
+by { convert cancel_epi f, simp, }
+lemma cancel_mono_id (f : X ⟶ Y) [mono f] {g : X ⟶ X} : (g ≫ f = f) ↔ g = 𝟙 X :=
+by { convert cancel_mono f, simp, }
+
+instance epi_comp {X Y Z : C} (f : X ⟶ Y) [epi f] (g : Y ⟶ Z) [epi g] : epi (f ≫ g) :=
+begin
+  split, intros Z a b w,
+  apply (cancel_epi g).1,
+  apply (cancel_epi f).1,
+  simpa using w,
+end
+instance mono_comp {X Y Z : C} (f : X ⟶ Y) [mono f] (g : Y ⟶ Z) [mono g] : mono (f ≫ g) :=
+begin
+  split, intros Z a b w,
+  apply (cancel_mono f).1,
+  apply (cancel_mono g).1,
+  simpa using w,
+end
+
+lemma mono_of_mono {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [mono (f ≫ g)] : mono f :=
+begin
+  split, intros Z a b w,
+  replace w := congr_arg (λ k, k ≫ g) w,
+  dsimp at w,
+  rw [category.assoc, category.assoc] at w,
+  exact (cancel_mono _).1 w,
+end
+
+lemma mono_of_mono_fac {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [mono h] (w : f ≫ g = h) : mono f :=
+by { resetI, subst h, exact mono_of_mono f g, }
+
+lemma epi_of_epi {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [epi (f ≫ g)] : epi g :=
+begin
+  split, intros Z a b w,
+  replace w := congr_arg (λ k, f ≫ k) w,
+  dsimp at w,
+  rw [←category.assoc, ←category.assoc] at w,
+  exact (cancel_epi _).1 w,
+end
+
+lemma epi_of_epi_fac {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [epi h] (w : f ≫ g = h) : epi g :=
+by { resetI, subst h, exact epi_of_epi f g, }
 end
 
 section

src/category_theory/limits/shapes/equalizers.lean

@@ -292,7 +292,7 @@ limit.lift (parallel_pair f g) (fork.of_ι k h)
 limit.hom_ext $ cone_parallel_pair_ext _ h
 
 /-- An equalizer morphism is a monomorphism -/
-lemma equalizer.ι_mono : mono (equalizer.ι f g) :=
+instance equalizer.ι_mono : mono (equalizer.ι f g) :=
 { right_cancellation := λ Z h k w, equalizer.hom_ext _ _ w }
 
 end
@@ -378,7 +378,7 @@ colimit.desc (parallel_pair f g) (cofork.of_π k h)
 colimit.hom_ext $ cocone_parallel_pair_ext _ h
 
 /-- A coequalizer morphism is an epimorphism -/
-lemma coequalizer.π_epi : epi (coequalizer.π f g) :=
+instance coequalizer.π_epi : epi (coequalizer.π f g) :=
 { left_cancellation := λ Z h k w, coequalizer.hom_ext _ _ w }
 
 end

src/category_theory/limits/shapes/images.lean

@@ -0,0 +1,217 @@
+/-
+Copyright (c) 2019 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison, Markus Himmel
+-/
+import category_theory.limits.shapes.equalizers
+
+/-!
+# Categorical images
+
+We define the categorical image of `f` as a factorisation `f = e ≫ m` through a monomorphism `m`,
+so that `m` factors through the `m'` in any other such factorisation.
+
+## Main statements
+
+* When `C` has equalizers, the morphism `m` is an epimorphism.
+
+## Future work
+* TODO: coimages, and abelian categories.
+* TODO: connect this with existing working in the group theory and ring theory libraries.
+
+-/
+
+universes v u
+
+open category_theory
+open category_theory.limits.walking_parallel_pair
+
+namespace category_theory.limits
+
+variables {C : Type u} [𝒞 : category.{v} C]
+include 𝒞
+
+variables {X Y : C} (f : X ⟶ Y)
+
+/-- A factorisation of a morphism `f = e ≫ m`, with `m` monic. -/
+structure mono_factorisation (f : X ⟶ Y) :=
+(I : C)
+(m : I ⟶ Y)
+[m_mono : mono.{v} m]
+(e : X ⟶ I)
+(fac' : e ≫ m = f . obviously)
+
+restate_axiom mono_factorisation.fac'
+attribute [simp, reassoc] mono_factorisation.fac
+
+namespace mono_factorisation
+
+/-- The obvious factorisation of a monomorphism through itself. -/
+def self [mono f] : mono_factorisation f :=
+{ I := X,
+  m := f,
+  e := 𝟙 X }
+
+-- I'm not sure we really need this, but the linter says that an inhabited instance ought to exist...
+instance [mono f] : inhabited (mono_factorisation f) := ⟨self f⟩
+
+/-- The morphism `m` in a factorisation `f = e ≫ m` through a monomorphism is uniquely determined. -/
+@[ext]
+lemma ext
+  {F F' : mono_factorisation f} (hI : F.I = F'.I) (hm : F.m = (eq_to_hom hI) ≫ F'.m) : F = F' :=
+begin
+  cases F, cases F',
+  cases hI,
+  simp at hm,
+  dsimp at F_fac' F'_fac',
+  congr,
+  { assumption },
+  { resetI, apply (cancel_mono F_m).1,
+    rw [F_fac', hm, F'_fac'], }
+end
+
+end mono_factorisation
+
+variable {f}
+
+/-- Data exhibiting that a given factorisation through a mono is initial. -/
+structure is_image (F : mono_factorisation f) :=
+(lift : Π (F' : mono_factorisation f), F.I ⟶ F'.I)
+(lift_fac' : Π (F' : mono_factorisation f), lift F' ≫ F'.m = F.m . obviously)
+
+restate_axiom is_image.lift_fac'
+attribute [simp, reassoc] is_image.lift_fac
+
+variable (f)
+
+namespace is_image
+
+/-- The trivial factorisation of a monomorphism satisfies the universal property. -/
+@[simps]
+def self [mono f] : is_image (mono_factorisation.self f) :=
+{ lift := λ F', F'.e }
+
+instance [mono f] : inhabited (is_image (mono_factorisation.self f)) :=
+⟨self f⟩
+
+variable {f}
+/-- Two factorisations through monomorphisms satisfying the universal property
+must factor through isomorphic objects. -/
+-- TODO this is another good candidate for a future `unique_up_to_canonical_iso`.
+@[simps]
+def iso_ext {F F' : mono_factorisation f} (hF : is_image F) (hF' : is_image F') : F.I ≅ F'.I :=
+{ hom := hF.lift F',
+  inv := hF'.lift F,
+  hom_inv_id' := begin haveI := F.m_mono, apply (cancel_mono F.m).1, simp end,
+  inv_hom_id' := begin haveI := F'.m_mono, apply (cancel_mono F'.m).1, simp end }
+
+end is_image
+
+/-- Data exhibiting that a morphism `f` has an image. -/
+class has_image (f : X ⟶ Y) :=
+(F : mono_factorisation f)
+(is_image : is_image F)
+
+variable [has_image f]
+
+/-- The chosen factorisation of `f` through a monomorphism. -/
+def image.mono_factorisation : mono_factorisation f := has_image.F f
+/-- The witness of the universal property for the chosen factorisation of `f` through a monomorphism. -/
+def image.is_image : is_image (image.mono_factorisation f) := has_image.is_image f
+
+/-- The categorical image of a morphism. -/
+def image : C := (image.mono_factorisation f).I
+/-- The inclusion of the image of a morphism into the target. -/
+def image.ι : image f ⟶ Y := (image.mono_factorisation f).m
+@[simp] lemma image.as_ι : (image.mono_factorisation f).m = image.ι f := rfl
+instance : mono (image.ι f) := (image.mono_factorisation f).m_mono
+/-- The 'corestriction' morphism from the source to the image. -/
+def image.c : X ⟶ image f := (image.mono_factorisation f).e
+@[simp] lemma image.as_c : (image.mono_factorisation f).e = image.c f := rfl
+@[simp] lemma image.c_ι : image.c f ≫ image.ι f = f := by erw (image.mono_factorisation f).fac
+
+/-- The map from the source to the image of a morphism. -/
+def factor_thru_image : X ⟶ image f := (image.mono_factorisation f).e
+@[simp, reassoc]
+lemma image.fac : factor_thru_image f ≫ image.ι f = f := (image.mono_factorisation f).fac'
+
+variable {f}
+/-- Any other factorisation of the morphism `f` through a monomorphism receives a map from the image. -/
+def image.lift (F' : mono_factorisation f) : image f ⟶ F'.I := (image.is_image f).lift F'
+@[simp, reassoc]
+lemma image.lift_fac (F' : mono_factorisation f) : image.lift F' ≫ F'.m = image.ι f :=
+(image.is_image f).lift_fac' F'
+
+-- TODO we could put a category structure on `mono_factorisation f`,
+-- with the morphisms being `g : I ⟶ I'` commuting with the `m`s
+-- (they then automatically commute with the `e`s)
+-- and show that an `image_of f` gives an initial object there
+-- (uniqueness of the lift comes for free).
+
+instance lift_mono (F' : mono_factorisation f) : mono.{v} (image.lift F') :=
+begin
+  split, intros Z a b w,
+  have w' : a ≫ image.ι f = b ≫ image.ι f :=
+  calc a ≫ image.ι f = a ≫ (image.lift F' ≫ F'.m) : by simp
+                 ... = (a ≫ image.lift F') ≫ F'.m : by rw [category.assoc]
+                 ... = (b ≫ image.lift F') ≫ F'.m : by rw w
+                 ... = b ≫ (image.lift F' ≫ F'.m) : by rw [←category.assoc]
+                 ... = b ≫ image.ι f : by simp,
+  exact (cancel_mono (image.ι f)).1 w',
+end
+lemma has_image.uniq
+  (F' : mono_factorisation f) (l : image f ⟶ F'.I) (w : l ≫ F'.m = image.ι f) :
+  l = image.lift F' :=
+begin
+  haveI := F'.m_mono,
+  apply (cancel_mono F'.m).1,
+  rw w,
+  simp,
+end
+
+/-- `has_images` represents a choice of image for every morphism -/
+class has_images :=
+(has_image : Π {X Y : C} (f : X ⟶ Y), has_image.{v} f)
+
+attribute [instance] has_images.has_image
+
+variable (f)
+/-- The image of a monomorphism is isomorphic to the source. -/
+def image_mono_iso_source [mono f] : image f ≅ X :=
+is_image.iso_ext (image.is_image f) (is_image.self f)
+
+@[simp, reassoc]
+lemma image_mono_iso_source_inv_ι [mono f] : (image_mono_iso_source f).inv ≫ image.ι f = f :=
+by simp [image_mono_iso_source]
+@[simp, reassoc]
+lemma image_mono_iso_source_hom_self [mono f] : (image_mono_iso_source f).hom ≫ f = image.ι f :=
+begin
+  conv { to_lhs, congr, skip, rw ←image_mono_iso_source_inv_ι f, },
+  rw [←category.assoc, iso.hom_inv_id, category.id_comp],
+end
+
+-- This is the proof from https://en.wikipedia.org/wiki/Image_(category_theory), which is taken from:
+-- Mitchell, Barry (1965), Theory of categories, MR 0202787, p.12, Proposition 10.1
+instance [has_equalizers.{v} C] : epi (factor_thru_image f) :=
+⟨λ Z g h w,
+begin
+  let q := equalizer.ι g h,
+  let e' := equalizer.lift _ _ _ w, -- TODO make more of the arguments to equalizer.lift implicit?
+  let F' : mono_factorisation f :=
+  { I := equalizer g h,
+    m := q ≫ image.ι f,
+    e := e' },
+  let v := image.lift F',
+  have t₀ : v ≫ q ≫ image.ι f = image.ι f := image.lift_fac F',
+  have t : v ≫ q = 𝟙 (image f) := (cancel_mono_id (image.ι f)).1 (by { convert t₀ using 1, rw category.assoc }),
+  -- The proof from wikipedia next proves `q ≫ v = 𝟙 _`,
+  -- and concludes that `equalizer g h ≅ image f`,
+  -- but this isn't necessary.
+  calc g = 𝟙 (image f) ≫ g : by rw [category.id_comp]
+     ... = v ≫ q ≫ g       : by rw [←t, category.assoc]
+     ... = v ≫ q ≫ h       : by rw [equalizer.condition g h]
+     ... = 𝟙 (image f) ≫ h : by rw [←category.assoc, t]
+     ... = h                : by rw [category.id_comp]
+end⟩
+
+end category_theory.limits