-
Notifications
You must be signed in to change notification settings - Fork 298
/
natural_isomorphism.lean
115 lines (90 loc) · 4.55 KB
/
natural_isomorphism.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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
/-
Copyright (c) 2017 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn
-/
import category_theory.functor_category
import category_theory.isomorphism
open category_theory
-- declare the `v`'s first; see `category_theory.category` for an explanation
universes v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
namespace category_theory
open nat_trans
variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D]
{E : Type u₃} [category.{v₃} E]
namespace iso
/-- The application of a natural isomorphism to an object. We put this definition in a different
namespace, so that we can use `α.app` -/
@[simp, reducible] def app {F G : C ⥤ D} (α : F ≅ G) (X : C) : F.obj X ≅ G.obj X :=
{ hom := α.hom.app X,
inv := α.inv.app X,
hom_inv_id' := begin rw [← comp_app, iso.hom_inv_id], refl end,
inv_hom_id' := begin rw [← comp_app, iso.inv_hom_id], refl end }
@[simp, reassoc]
lemma hom_inv_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) :
α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X) :=
congr_fun (congr_arg nat_trans.app α.hom_inv_id) X
@[simp, reassoc]
lemma inv_hom_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) :
α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X) :=
congr_fun (congr_arg nat_trans.app α.inv_hom_id) X
end iso
namespace nat_iso
open category_theory.category category_theory.functor
@[simp] lemma trans_app {F G H : C ⥤ D} (α : F ≅ G) (β : G ≅ H) (X : C) :
(α ≪≫ β).app X = α.app X ≪≫ β.app X := rfl
lemma app_hom {F G : C ⥤ D} (α : F ≅ G) (X : C) : (α.app X).hom = α.hom.app X := rfl
lemma app_inv {F G : C ⥤ D} (α : F ≅ G) (X : C) : (α.app X).inv = α.inv.app X := rfl
variables {F G : C ⥤ D}
instance hom_app_is_iso (α : F ≅ G) (X : C) : is_iso (α.hom.app X) :=
{ inv := α.inv.app X,
hom_inv_id' := begin rw [←comp_app, iso.hom_inv_id, ←id_app] end,
inv_hom_id' := begin rw [←comp_app, iso.inv_hom_id, ←id_app] end }
instance inv_app_is_iso (α : F ≅ G) (X : C) : is_iso (α.inv.app X) :=
{ inv := α.hom.app X,
hom_inv_id' := begin rw [←comp_app, iso.inv_hom_id, ←id_app] end,
inv_hom_id' := begin rw [←comp_app, iso.hom_inv_id, ←id_app] end }
variables {X Y : C}
lemma naturality_1 (α : F ≅ G) (f : X ⟶ Y) :
(α.inv.app X) ≫ (F.map f) ≫ (α.hom.app Y) = G.map f :=
begin erw [naturality, ←category.assoc, is_iso.hom_inv_id, category.id_comp] end
lemma naturality_2 (α : F ≅ G) (f : X ⟶ Y) :
(α.hom.app X) ≫ (G.map f) ≫ (α.inv.app Y) = F.map f :=
begin erw [naturality, ←category.assoc, is_iso.hom_inv_id, category.id_comp] end
def is_iso_of_is_iso_app (α : F ⟶ G) [∀ X : C, is_iso (α.app X)] : is_iso α :=
{ inv :=
{ app := λ X, inv (α.app X),
naturality' := λ X Y f,
begin
have h := congr_arg (λ f, inv (α.app X) ≫ (f ≫ inv (α.app Y))) (α.naturality f).symm,
simp only [is_iso.inv_hom_id_assoc, is_iso.hom_inv_id, assoc, comp_id, cancel_mono] at h,
exact h
end } }
instance is_iso_of_is_iso_app' (α : F ⟶ G) [H : ∀ X : C, is_iso (nat_trans.app α X)] : is_iso α :=
@nat_iso.is_iso_of_is_iso_app _ _ _ _ _ _ α H
-- TODO can we make this an instance?
def is_iso_app_of_is_iso (α : F ⟶ G) [is_iso α] (X) : is_iso (α.app X) :=
{ inv := (inv α).app X,
hom_inv_id' := congr_fun (congr_arg nat_trans.app (is_iso.hom_inv_id α)) X,
inv_hom_id' := congr_fun (congr_arg nat_trans.app (is_iso.inv_hom_id α)) X }
def of_components (app : ∀ X : C, F.obj X ≅ G.obj X)
(naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f) :
F ≅ G :=
as_iso { app := λ X, (app X).hom }
@[simp] lemma of_components.app (app' : ∀ X : C, F.obj X ≅ G.obj X) (naturality) (X) :
(of_components app' naturality).app X = app' X :=
by tidy
@[simp] lemma of_components.hom_app (app : ∀ X : C, F.obj X ≅ G.obj X) (naturality) (X) :
(of_components app naturality).hom.app X = (app X).hom := rfl
@[simp] lemma of_components.inv_app (app : ∀ X : C, F.obj X ≅ G.obj X) (naturality) (X) :
(of_components app naturality).inv.app X = (app X).inv := rfl
def hcomp {F G : C ⥤ D} {H I : D ⥤ E} (α : F ≅ G) (β : H ≅ I) : F ⋙ H ≅ G ⋙ I :=
begin
refine ⟨α.hom ◫ β.hom, α.inv ◫ β.inv, _, _⟩,
{ ext, rw [←nat_trans.exchange], simp, refl },
ext, rw [←nat_trans.exchange], simp, refl
end
-- declare local notation for nat_iso.hcomp
localized "infix ` ■ `:80 := category_theory.nat_iso.hcomp" in category
end nat_iso
end category_theory