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_.