<commit_before>/-
Copyright (c) 2019 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import category_theory.limits.shapes.terminal
import category_theory.limits.shapes.binary_products
import category_theory.limits.shapes.products
import category_theory.limits.shapes.images
import category_theory.isomorphism_classes

/-!
# Zero morphisms and zero objects

A category "has zero morphisms" if there is a designated "zero morphism" in each morphism space,
and compositions of zero morphisms with anything give the zero morphism. (Notice this is extra
structure, not merely a property.)

A category "has a zero object" if it has an object which is both initial and terminal. Having a
zero object provides zero morphisms, as the unique morphisms factoring through the zero object.

## References

* https://en.wikipedia.org/wiki/Zero_morphism
* [F. Borceux, *Handbook of Categorical Algebra 2*][borceux-vol2]
-/

noncomputable theory

universes v u

open category_theory
open category_theory.category

namespace category_theory.limits

variables (C : Type u) [category.{v} C]

/-- A category "has zero morphisms" if there is a designated "zero morphism" in each morphism space,
and compositions of zero morphisms with anything give the zero morphism. -/
class has_zero_morphisms :=
[has_zero : Π X Y : C, has_zero (X ⟶ Y)]
(comp_zero' : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ (0 : Y ⟶ Z) = (0 : X ⟶ Z) . obviously)
(zero_comp' : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), (0 : X ⟶ Y) ≫ f = (0 : X ⟶ Z) . obviously)

attribute [instance] has_zero_morphisms.has_zero
restate_axiom has_zero_morphisms.comp_zero'
restate_axiom has_zero_morphisms.zero_comp'

variables {C}

@[simp] lemma comp_zero [has_zero_morphisms C] {X Y : C} {f : X ⟶ Y} {Z : C} :
  f ≫ (0 : Y ⟶ Z) = (0 : X ⟶ Z) := has_zero_morphisms.comp_zero f Z
@[simp] lemma zero_comp [has_zero_morphisms C] {X : C} {Y Z : C} {f : Y ⟶ Z} :
  (0 : X ⟶ Y) ≫ f = (0 : X ⟶ Z) := has_zero_morphisms.zero_comp X f

instance has_zero_morphisms_pempty : has_zero_morphisms (discrete pempty) :=
{ has_zero := by tidy }

instance has_zero_morphisms_punit : has_zero_morphisms (discrete punit) :=
{ has_zero := by tidy }

namespace has_zero_morphisms
variables {C}

/-- This lemma will be immediately superseded by `ext`, below. -/
private lemma ext_aux (I J : has_zero_morphisms C)
  (w : ∀ X Y : C, (@has_zero_morphisms.has_zero _ _ I X Y).zero =
    (@has_zero_morphisms.has_zero _ _ J X Y).zero) : I = J :=
begin
  casesI I, casesI J,
  congr,
  { ext X Y,
    exact w X Y },
  { apply proof_irrel_heq, },
  { apply proof_irrel_heq, }
end

/--
If you're tempted to use this lemma "in the wild", you should probably
carefully consider whether you've made a mistake in allowing two
instances of `has_zero_morphisms` to exist at all.

See, particularly, the note on `zero_morphisms_of_zero_object` below.
-/
lemma ext (I J : has_zero_morphisms C) : I = J :=
begin
  apply ext_aux,
  intros X Y,
  rw ←@has_zero_morphisms.comp_zero _ _ I X X (@has_zero_morphisms.has_zero _ _ J X X).zero,
  rw @has_zero_morphisms.zero_comp _ _ J,
end

instance : subsingleton (has_zero_morphisms C) :=
⟨ext⟩

end has_zero_morphisms

open has_zero_morphisms

section
variables {C} [has_zero_morphisms C]

lemma zero_of_comp_mono {X Y Z : C} {f : X ⟶ Y} (g : Y ⟶ Z) [mono g] (h : f ≫ g = 0) : f = 0 :=
by { rw [←zero_comp, cancel_mono] at h, exact h }

lemma zero_of_epi_comp {X Y Z : C} (f : X ⟶ Y) {g : Y ⟶ Z} [epi f] (h : f ≫ g = 0) : g = 0 :=
by { rw [←comp_zero, cancel_epi] at h, exact h }

lemma eq_zero_of_image_eq_zero {X Y : C} {f : X ⟶ Y} [has_image f] (w : image.ι f = 0) : f = 0 :=
by rw [←image.fac f, w, has_zero_morphisms.comp_zero]

lemma nonzero_image_of_nonzero {X Y : C} {f : X ⟶ Y} [has_image f] (w : f ≠ 0) : image.ι f ≠ 0 :=
λ h, w (eq_zero_of_image_eq_zero h)
end

section
universes v' u'
variables (D : Type u') [category.{v'} D]

variables [has_zero_morphisms C] [has_zero_morphisms D]

lemma equivalence_preserves_zero_morphisms (F : C ≌ D) (X Y : C) :
  F.functor.map (0 : X ⟶ Y) = (0 : F.functor.obj X ⟶ F.functor.obj Y) :=
begin
  have t : F.functor.map (0 : X ⟶ Y) =
    F.functor.map (0 : X ⟶ Y) ≫ (0 : F.functor.obj Y ⟶ F.functor.obj Y),
  { apply faithful.map_injective (F.inverse),
    rw [functor.map_comp, equivalence.inv_fun_map],
    dsimp,
    rw [zero_comp, comp_zero, zero_comp], },
  exact t.trans (by simp)
end

@[simp] lemma is_equivalence_preserves_zero_morphisms (F : C ⥤ D) [is_equivalence F] (X Y : C) :<commit_msg>feat(category_theory/limits/zero): functor categories have zero morphisms (#6928)<commit_after>/-
Copyright (c) 2019 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import category_theory.limits.shapes.terminal
import category_theory.limits.shapes.binary_products
import category_theory.limits.shapes.products
import category_theory.limits.shapes.images
import category_theory.isomorphism_classes

/-!
# Zero morphisms and zero objects

A category "has zero morphisms" if there is a designated "zero morphism" in each morphism space,
and compositions of zero morphisms with anything give the zero morphism. (Notice this is extra
structure, not merely a property.)

A category "has a zero object" if it has an object which is both initial and terminal. Having a
zero object provides zero morphisms, as the unique morphisms factoring through the zero object.

## References

* https://en.wikipedia.org/wiki/Zero_morphism
* [F. Borceux, *Handbook of Categorical Algebra 2*][borceux-vol2]
-/

noncomputable theory

universes v u

open category_theory
open category_theory.category

namespace category_theory.limits

variables (C : Type u) [category.{v} C]

/-- A category "has zero morphisms" if there is a designated "zero morphism" in each morphism space,
and compositions of zero morphisms with anything give the zero morphism. -/
class has_zero_morphisms :=
[has_zero : Π X Y : C, has_zero (X ⟶ Y)]
(comp_zero' : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ (0 : Y ⟶ Z) = (0 : X ⟶ Z) . obviously)
(zero_comp' : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), (0 : X ⟶ Y) ≫ f = (0 : X ⟶ Z) . obviously)

attribute [instance] has_zero_morphisms.has_zero
restate_axiom has_zero_morphisms.comp_zero'
restate_axiom has_zero_morphisms.zero_comp'

variables {C}

@[simp] lemma comp_zero [has_zero_morphisms C] {X Y : C} {f : X ⟶ Y} {Z : C} :
  f ≫ (0 : Y ⟶ Z) = (0 : X ⟶ Z) := has_zero_morphisms.comp_zero f Z
@[simp] lemma zero_comp [has_zero_morphisms C] {X : C} {Y Z : C} {f : Y ⟶ Z} :
  (0 : X ⟶ Y) ≫ f = (0 : X ⟶ Z) := has_zero_morphisms.zero_comp X f

instance has_zero_morphisms_pempty : has_zero_morphisms (discrete pempty) :=
{ has_zero := by tidy }

instance has_zero_morphisms_punit : has_zero_morphisms (discrete punit) :=
{ has_zero := by tidy }

namespace has_zero_morphisms
variables {C}

/-- This lemma will be immediately superseded by `ext`, below. -/
private lemma ext_aux (I J : has_zero_morphisms C)
  (w : ∀ X Y : C, (@has_zero_morphisms.has_zero _ _ I X Y).zero =
    (@has_zero_morphisms.has_zero _ _ J X Y).zero) : I = J :=
begin
  casesI I, casesI J,
  congr,
  { ext X Y,
    exact w X Y },
  { apply proof_irrel_heq, },
  { apply proof_irrel_heq, }
end

/--
If you're tempted to use this lemma "in the wild", you should probably
carefully consider whether you've made a mistake in allowing two
instances of `has_zero_morphisms` to exist at all.

See, particularly, the note on `zero_morphisms_of_zero_object` below.
-/
lemma ext (I J : has_zero_morphisms C) : I = J :=
begin
  apply ext_aux,
  intros X Y,
  rw ←@has_zero_morphisms.comp_zero _ _ I X X (@has_zero_morphisms.has_zero _ _ J X X).zero,
  rw @has_zero_morphisms.zero_comp _ _ J,
end

instance : subsingleton (has_zero_morphisms C) :=
⟨ext⟩

end has_zero_morphisms

open has_zero_morphisms

section
variables {C} [has_zero_morphisms C]

lemma zero_of_comp_mono {X Y Z : C} {f : X ⟶ Y} (g : Y ⟶ Z) [mono g] (h : f ≫ g = 0) : f = 0 :=
by { rw [←zero_comp, cancel_mono] at h, exact h }

lemma zero_of_epi_comp {X Y Z : C} (f : X ⟶ Y) {g : Y ⟶ Z} [epi f] (h : f ≫ g = 0) : g = 0 :=
by { rw [←comp_zero, cancel_epi] at h, exact h }

lemma eq_zero_of_image_eq_zero {X Y : C} {f : X ⟶ Y} [has_image f] (w : image.ι f = 0) : f = 0 :=
by rw [←image.fac f, w, has_zero_morphisms.comp_zero]

lemma nonzero_image_of_nonzero {X Y : C} {f : X ⟶ Y} [has_image f] (w : f ≠ 0) : image.ι f ≠ 0 :=
λ h, w (eq_zero_of_image_eq_zero h)
end

section
universes v' u'
variables (D : Type u') [category.{v'} D]

variables [has_zero_morphisms D]

instance : has_zero_morphisms (C ⥤ D) :=
{ has_zero := λ F G, ⟨{ app := λ X, 0, }⟩ }

@[simp] lemma zero_app (F G : C ⥤ D) (j : C) : (0 : F ⟶ G).app j = 0 := rfl

variables [has_zero_morphisms C]

lemma equivalence_preserves_zero_morphisms (F : C ≌ D) (X Y : C) :
  F.functor.map (0 : X ⟶ Y) = (0 : F.functor.obj X ⟶ F.functor.obj Y) :=
begin
  have t : F.functor.map (0 : X ⟶ Y) =
    F.functor.map (0 : X ⟶ Y) ≫ (0 : F.functor.obj Y ⟶ F.functor.obj Y),
  { apply faithful.map_injective (F.inverse),
    rw [functor.map_comp, equivalence.inv_fun_map],
    dsimp,
    rw [zero_comp, comp_zero, zero_comp], },
  exact t.trans (by simp)
end

@[simp] lemma is_equivalence_preserves_zero_morphisms (F : C ⥤ D) [is_equivalence F] (X Y : C) :
{'fraction_non_alphanumeric': 0.12202444778039888, 'fraction_numerical': 0.006969761955822432, 'mean_word_length': 3.8176652892561984, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 2, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '663980', 'n_tokens_mistral': 3921, 'n_tokens_neox': 3629, 'n_words': 1271}