-
Notifications
You must be signed in to change notification settings - Fork 300
/
EpiMono.lean
61 lines (42 loc) · 1.73 KB
/
EpiMono.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
/-
Copyright (c) 2024 Joël Riou. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joël Riou
-/
import Mathlib.CategoryTheory.Limits.Constructions.EpiMono
import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-!
# Monomorphisms and epimorphisms in functor categories
A natural transformation `f : F ⟶ G` between functors `K ⥤ C`
is a mono (resp. epi) iff for all `k : K`, `f.app k` is,
at least when `C` has pullbacks (resp. pushouts),
see `NatTrans.mono_iff_mono_app` and `NatTrans.epi_iff_epi_app`.
-/
universe v v' v'' u u' u''
namespace CategoryTheory
open Limits
variable {K : Type u} [Category.{v} K] {C : Type u'} [Category.{v'} C]
{D : Type u''} [Category.{v''} D] {F G : K ⥤ C} (f : F ⟶ G)
section
variable [HasPullbacks C]
instance [Mono f] (k : K) : Mono (f.app k) :=
inferInstanceAs (Mono (((evaluation K C).obj k).map f))
lemma NatTrans.mono_iff_mono_app : Mono f ↔ ∀ (k : K), Mono (f.app k) :=
⟨fun _ ↦ inferInstance, fun _ ↦ mono_of_mono_app _⟩
instance [Mono f] (H : C ⥤ D) [H.PreservesMonomorphisms] :
Mono (whiskerRight f H) := by
have : ∀ X, Mono ((whiskerRight f H).app X) := by intros; dsimp; infer_instance
apply NatTrans.mono_of_mono_app
end
section
variable [HasPushouts C]
instance [Epi f] (k : K) : Epi (f.app k) :=
inferInstanceAs (Epi (((evaluation K C).obj k).map f))
lemma NatTrans.epi_iff_epi_app : Epi f ↔ ∀ (k : K), Epi (f.app k) :=
⟨fun _ ↦ inferInstance, fun _ ↦ epi_of_epi_app _⟩
instance [Epi f] (H : C ⥤ D) [H.PreservesEpimorphisms] :
Epi (whiskerRight f H) := by
have : ∀ X, Epi ((whiskerRight f H).app X) := by intros; dsimp; infer_instance
apply NatTrans.epi_of_epi_app
end
end CategoryTheory