-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathHom.v
122 lines (102 loc) · 4.11 KB
/
Hom.v
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
116
117
118
119
120
121
122
Require Import FunctionalExtensionality.
Require Export SpecializedCategory Functor Duals SetCategory ProductCategory.
Require Import Common.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.
Local Open Scope category_scope.
(*
We could do covariant and contravariant as
Section covariant_contravariant.
Local Arguments InducedProductSndFunctor / _ _ _ _ _ _ _ _ _ _ _.
Definition CovariantHomFunctor `(C : @SpecializedCategory objC) (A : OppositeCategory C) :=
Eval simpl in ((HomFunctor C) [ A, - ])%functor.
Definition ContravariantHomFunctor `(C : @SpecializedCategory objC) (A : C) := ((HomFunctor C) [ -, A ])%functor.
Definition CovariantHomSetFunctor `(C : @LocallySmallSpecializedCategory objC morC) (A : OppositeCategory C) := ((HomSetFunctor C) [ A, - ])%functor.
Definition ContravariantHomSetFunctor `(C : @LocallySmallSpecializedCategory objC morC) (A : C) := ((HomSetFunctor C) [ -, A ])%functor.
End covariant_contravariant.
but that would introduce an extra identity morphism which some tactics
have a bit of trouble with. *sigh*
*)
Section HomFunctor.
Context `(C : @SpecializedCategory objC).
Let COp := OppositeCategory C.
Section Covariant.
Variable A : COp.
Definition CovariantHomFunctor : SpecializedFunctor C TypeCat.
refine (Build_SpecializedFunctor C TypeCat
(fun X : C => C.(Morphism) A X : TypeCat)
(fun X Y f => (fun g : C.(Morphism) A X => Compose f g))
_
_
);
abstract (simpl; intros; repeat (apply functional_extensionality_dep; intro); auto with morphism).
Defined.
End Covariant.
Section Contravariant.
Variable B : C.
Definition ContravariantHomFunctor : SpecializedFunctor COp TypeCat.
refine (Build_SpecializedFunctor COp TypeCat
(fun X : COp => COp.(Morphism) B X : TypeCat)
(fun X Y (h : COp.(Morphism) X Y) => (fun g : COp.(Morphism) B X => Compose h g))
_
_
);
abstract (simpl; intros; repeat (apply functional_extensionality_dep; intro); auto with morphism).
Defined.
End Contravariant.
Definition hom_functor_object_of (c'c : COp * C) := C.(Morphism) (fst c'c) (snd c'c) : TypeCat.
Definition hom_functor_morphism_of (s's : (COp * C)%type) (d'd : (COp * C)%type) (hf : (COp * C).(Morphism) s's d'd) :
TypeCat.(Morphism) (hom_functor_object_of s's) (hom_functor_object_of d'd).
unfold hom_functor_object_of in *.
destruct s's as [ s' s ], d'd as [ d' d ].
destruct hf as [ h f ].
intro g.
exact (Compose f (Compose g h)).
Defined.
Definition HomFunctor : SpecializedFunctor (COp * C) TypeCat.
refine (Build_SpecializedFunctor (COp * C) TypeCat
(fun c'c : COp * C => C.(Morphism) (fst c'c) (snd c'c) : TypeCat)
(fun X Y (hf : (COp * C).(Morphism) X Y) => hom_functor_morphism_of hf)
_
_
);
abstract (
intros; simpl in *; destruct_hypotheses;
simpl in *;
repeat (apply functional_extensionality_dep; intro);
autorewrite with morphism; reflexivity
).
Defined.
End HomFunctor.
Section SplitHomFunctor.
Context `(C : @SpecializedCategory objC).
Let COp := OppositeCategory C.
Lemma SplitHom (X Y : COp * C) : forall gh,
MorphismOf (HomFunctor C) (s := X) (d := Y) gh =
(Compose
(MorphismOf (ContravariantHomFunctor C (snd Y)) (s := fst X) (d := fst Y) (fst gh))
(MorphismOf (CovariantHomFunctor C (fst X)) (s := snd X) (d := snd Y) (snd gh))).
Proof.
destruct X, Y.
intro gh; destruct gh.
simpl in *.
apply functional_extensionality_dep; intro.
autorewrite with morphism.
reflexivity.
Qed.
Lemma SplitHom' (X Y : COp * C) : forall gh,
MorphismOf (HomFunctor C) (s := X) (d := Y) gh =
(Compose
(MorphismOf (CovariantHomFunctor C (fst Y)) (s := snd X) (d := snd Y) (snd gh))
(MorphismOf (ContravariantHomFunctor C (snd X)) (s := fst X) (d := fst Y) (fst gh))).
Proof.
destruct X, Y.
intro gh; destruct gh.
simpl in *.
apply functional_extensionality_dep; intro.
autorewrite with morphism.
reflexivity.
Qed.
End SplitHomFunctor.