Standard definitions in Category Theory. |
This file collects the definitions of special objects and arrows: mono/epi morphism, inital/final object, equalizers, kernels and cokernels. |
Require
Export
cat.
Implicit Arguments On.
Module
Universal.
Export
Misc.
Export
Cat.
Mono and Epi morphisms |
Section
Mono_Epi.
Variable
A:Cat; x,y:A; f:(mor x y).
Definition
is_mono : Prop :=
(z:A; u1,u2:(mor z x)) (oo f u1)==(oo f u2) -> u1==u2.
Definition
is_epi : Prop :=
(z:A; u1,u2:(mor y z)) (oo u1 f)==(oo u2 f) -> u1==u2.
End
Mono_Epi.
One side and two sides invese morphisms |
Section
Inv.
Variable
A:Cat; x,y:A; f:(mor x y).
Definition
is_inv_sx [g:(mor y x)] : Prop :=
(oo g f)==(ii x).
Record
Inv_Sx : Type := {
inv_sx_mor :> (mor y x);
ax_inv_sx_prop : (is_inv_sx inv_sx_mor)
}.
Lemma
inv_sx_prop : (g:Inv_Sx) (oo g f)==(ii x).
Proof
.
Intros; Apply (ax_inv_sx_prop g).
Qed
.
Lemma
mono_of_inv_sx : (g:Inv_Sx) (is_mono f).
Proof
.
Unfold is_mono; Intros.
Rewrite <- (ii_sx u1).
Rewrite <- (inv_sx_prop g).
Rewrite <- oo_assoc.
Rewrite H.
Rewrite oo_assoc; Rewrite inv_sx_prop; Auto.
Qed
.
Definition
is_inv_dx [g:(mor y x)] : Prop :=
(oo f g)==(ii y).
Record
Inv_Dx : Type := {
inv_dx_mor :> (mor y x);
ax_inv_dx_prop : (is_inv_dx inv_dx_mor)
}.
Lemma
inv_dx_prop : (g:Inv_Dx) (oo f g)==(ii y).
Proof
.
Intros; Apply (ax_inv_dx_prop g).
Qed
.
Lemma
epi_of_inv_dx : (g:Inv_Dx) (is_epi f).
Proof
.
Unfold is_epi; Intros.
Rewrite <- (ii_dx u1).
Rewrite <- (inv_dx_prop g).
Rewrite oo_assoc.
Rewrite H.
Rewrite <- oo_assoc; Rewrite inv_dx_prop; Auto.
Qed
.
Record
Inv_Theory [g:(mor y x)] : Prop := {
ax_inv_prop_sx : (is_inv_sx g);
ax_inv_prop_dx : (is_inv_dx g)
}.
Record
Inv : Type := {
inv_mor :> (mor y x);
inv_theory : (Inv_Theory inv_mor)
}.
Lemma
inv_prop_sx : (g:Inv) (oo g f)==(ii x).
Proof
.
Intros; NewDestruct (inv_theory g); Assumption.
Qed
.
Lemma
inv_prop_dx : (g:Inv) (oo f g)==(ii y).
Proof
.
Intros; NewDestruct (inv_theory g); Assumption.
Qed
.
Hints
Resolve inv_sx_prop mono_of_inv_sx inv_dx_prop epi_of_inv_dx
inv_prop_sx inv_prop_dx.
Definition
inv_sx_of_inv [g:Inv] : Inv_Sx.
Proof
.
Intros; Split with (inv_mor g).
Unfold is_inv_sx; Apply inv_prop_sx.
Defined
.
Definition
inv_dx_of_inv [g:Inv] : Inv_Dx.
Proof
.
Intros; Split with (inv_mor g).
Unfold is_inv_dx; Apply inv_prop_dx.
Defined
.
Lemma
mono_of_inv : (g:Inv)(is_mono f).
Proof
.
Intros; Apply mono_of_inv_sx.
Apply inv_sx_of_inv.
Exact g.
Qed
.
Lemma
epi_of_inv : (g:Inv)(is_epi f).
Proof
.
Intros; Apply epi_of_inv_dx.
Apply inv_dx_of_inv.
Exact g.
Qed
.
Lemma
inv_unique : (g,h:Inv) g==h.
Proof
.
Intros.
Assert U : (inv_mor g)==(inv_mor h).
Rewrite <- (ii_sx g).
Rewrite <- (inv_prop_sx h).
Rewrite <- oo_assoc.
Rewrite inv_prop_dx; Trivial.
NewDestruct g; NewDestruct h.
Simpl in U.
NewDestruct U.
Assert U: inv_theory0==inv_theory1.
Apply proof_irrelevance.
Simpl.
NewDestruct U.
Reflexivity.
Qed
.
End
Inv.
Hints
Resolve inv_sx_prop mono_of_inv_sx inv_dx_prop epi_of_inv_dx
inv_prop_sx inv_prop_dx mono_of_inv epi_of_inv.
Universal objects |
Section
Final.
Variable
A:Cat.
Section
Final_Theory.
Variable
u:A; j : (x:A) (mor x u).
Definition
Final_Theory : Prop :=
(x:A; f:(mor x u)) (j x)==f.
End
Final_Theory.
Record
Final : Type := {
final_obj : A;
final : (x:A) (mor x final_obj);
final_theory : (Final_Theory final)
}.
Coercion Local
final_obj : Final >-> obj.
Section
Final_Facts.
Variable
j:Final.
Local
Hj := (!final_theory j).
Lemma
final_eq : (x:A; f:(mor x j)) (final j x)==f.
Proof
.
Unfold Final_Theory in Hj; Auto.
Qed
.
End
Final_Facts.
Hints
Resolve final_eq.
Lemma
final_f_eq_g : (j:Final; x:A; f,g:(mor x j)) f==g.
Proof
.
Intros.
Rewrite <- final_eq with f:=f.
Trivial.
Qed
.
Lemma
final_extens : (s,t:Final)
(final_obj s)==(final_obj t) -> s==t.
Proof
.
Intros s t.
Assert L := (!final_f_eq_g t).
NewDestruct s; NewDestruct t; Simpl.
NewDestruct 1.
Rename final_obj0 into v.
Assert U : final0==final1.
Apply extensionality with T:=[x:A](mor x v).
Intros.
Apply L.
NewDestruct U.
Assert U : final_theory0==final_theory1.
Apply proof_irrelevance.
NewDestruct U; Reflexivity.
Qed
.
Definition
final_isom [j,k:Final] : (mor j k) := (final k j).
Lemma
final_isom_eq : (j,k:Final)
(oo (final_isom k j) (final_isom j k))==(ii j).
Proof
.
Intros; Apply final_f_eq_g.
Qed
.
Definition
final_isom_inv [j,k:Final] : (Inv (final_isom j k)).
Proof
.
Intros; Split with (final_isom k j).
Abstract Split; Unfold is_inv_sx is_inv_dx; Apply final_isom_eq.
Defined
.
End
Final.
Hints
Resolve final_eq final_isom_eq.
Section
Initial.
Variable
A:Cat.
Section
Initial_Theory.
Variable
u:A; j : (x:A) (mor u x).
Definition
Initial_Theory : Prop :=
(x:A; f:(mor u x)) (j x)==f.
End
Initial_Theory.
Record
Initial : Type := {
initial_obj : A;
initial : (x:A) (mor initial_obj x);
initial_theory : (Initial_Theory initial)
}.
Coercion Local
initial_obj : Initial >-> obj.
Section
Initial_Facts.
Variable
j:Initial.
Local
Hj := (!initial_theory j).
Lemma
initial_eq : (x:A; f:(mor j x)) (initial j x)==f.
Proof
.
Unfold Initial_Theory in Hj; Auto.
Qed
.
Lemma
initial_src_eq : (x:A)(trg (initial j x))==x.
Proof
.
Reflexivity.
Qed
.
End
Initial_Facts.
Hints
Resolve initial_src_eq initial_eq.
Lemma
initial_f_eq_g : (j:Initial; x:A; f,g:(mor j x)) f==g.
Proof
.
Intros.
Rewrite <- initial_eq with f:=f.
Trivial.
Qed
.
Lemma
initial_extens : (s,t:Initial)
(initial_obj s)==(initial_obj t) -> s==t.
Proof
.
Intros s t.
Assert L := (!initial_f_eq_g t).
NewDestruct s; NewDestruct t; Simpl.
NewDestruct 1.
Rename initial_obj0 into v.
Assert U : initial0==initial1.
Apply extensionality with T:=[x:A](mor v x).
Intros.
Apply L.
NewDestruct U.
Assert U : initial_theory0==initial_theory1.
Apply proof_irrelevance.
NewDestruct U; Reflexivity.
Qed
.
Definition
initial_isom [j,k:Initial] : (mor j k) := (initial j k).
Lemma
initial_isom_eq : (j,k:Initial)
(oo (initial_isom k j) (initial_isom j k))==(ii j).
Proof
.
Intros; Apply initial_f_eq_g.
Qed
.
Definition
initial_isom_inv [j,k:Initial] : (Inv (initial_isom j k)).
Proof
.
Intros; Split with (initial_isom k j).
Abstract Split; Unfold is_inv_sx is_inv_dx; Apply initial_isom_eq.
Defined
.
End
Initial.
Hints
Resolve initial_src_eq initial_eq initial_isom_eq.
Section
Zero.
Variable
A:Cat.
Section
Zero_Theory.
Variable
u:A; j1 : (x:A) (mor u x); j2 : (x:A) (mor x u).
Record
Zero_Theory : Prop := {
ax_zero_initial_eq : (x:A; f:(mor u x)) (j1 x)==f;
ax_zero_final_eq : (x:A; f:(mor x u)) (j2 x)==f
}.
End
Zero_Theory.
Record
Zero : Type := {
zero_obj :> A;
zero_initial : (x:A) (mor zero_obj x);
zero_final : (x:A) (mor x zero_obj);
zero_theory : (Zero_Theory zero_initial zero_final)
}.
Definition
final_of_zero [j:Zero] : (Final A).
Proof
.
Intros; Split with final:=(zero_final j).
Abstract Unfold Final_Theory; NewDestruct (zero_theory j); Auto.
Defined
.
Coercion final_of_zero : Zero >-> Final.
Definition
initial_of_zero [j:Zero] : (Initial A).
Proof
.
Intros; Split with initial:=(zero_initial j).
Abstract Unfold Initial_Theory; NewDestruct (zero_theory j); Auto.
Defined
.
Coercion initial_of_zero : Zero >-> Initial.
End
Zero.
End
Universal.