Module product

Products in a category. Notations: (Product f g) type of a producto over two arrows f:(mor u x) and g:(mor u y); (proj1 u) and (proj2 u) projection associated to a product u:(Product f g); (product u h1 h2) morphism in (mor v u) associated to a pair of arrows h1:(mor v x) and h2:(mor v y); product_eq product_sx_eq product_dx_eq equalities implied by (and equivalent to) the universal property of the product; product_isom natural isomorphism between two products; has_product the property of categories which has products. product_comm isomorphism given by the commutativity of products; product_assoc isomorphism given by the associativity of products;

Require Export universal.

Implicit Arguments On.

Module Product.

Export Universal.

Section Product.

Variable A:Cat.

Variable x,y:A.

Section Product_Theory.

Variable u:A; px:(mor u x); py:(mor u y).

Variable product : (v:A; fx:(mor v x); fy:(mor v y)) (mor v u).

Record Product_Theory : Prop := {
  ax_product_dx_eq : (v:A; fx:(mor v x); fy:(mor v y))
   (oo px (product fx fy))==fx;
  ax_product_sx_eq : (v:A; fx:(mor v x); fy:(mor v y))
   (oo py (product fx fy))==fy;
  ax_product_eq : (v:A; f:(mor v u))
   (product (oo px f) (oo py f))==f
 }.

End Product_Theory.

Record Product : Type := {
  product_obj :> A;
  proj1 : (mor product_obj x);
  proj2 : (mor product_obj y);
  product : (v:A; fx:(mor v x); fy:(mor v y)) (mor v product_obj);
  product_theory : (Product_Theory proj1 proj2 product)
 }.

Section Product_Facts.

Variable p:Product.

Local p_th := (product_theory p).

Lemma product_sx_eq : (v:A; fx:(mor v x); fy:(mor v y))
 (oo (proj1 p) (product p fx fy))==fx.
Proof.
  NewDestruct p_th; Trivial.
Qed.

Lemma product_dx_eq : (v:A; fx:(mor v x); fy:(mor v y))
 (oo (proj2 p) (product p fx fy))==fy.
Proof.
  NewDestruct p_th; Trivial.
Qed.

Lemma product_eq : (v:A; f:(mor v p))
 (product p (oo (proj1 p) f) (oo (proj2 p) f))==f.
Proof.
  NewDestruct p_th; Trivial.
Qed.

Lemma product_f_eq_g : (u:A; f,g:(mor u p))
 (oo (proj1 p) f)==(oo (proj1 p) g) -> (oo (proj2 p) f)==(oo (proj2 p) g) ->
 f==g.
Proof.
  Intros.
  Rewrite <- product_eq with f:=g.
  NewDestruct H; NewDestruct H0.
  Rewrite product_eq.
  Reflexivity.
Qed.

End Product_Facts.

Definition product_isom [p,q:Product] : (mor p q) :=
 (product q (proj1 p) (proj2 p)).

Lemma product_isom_eq : (p,q:Product)
 (oo (product_isom q p) (product_isom p q))==(ii p).
Proof.
  Unfold product_isom; Intros.
  Apply product_f_eq_g; Rewrite oo_assoc.
  Do 2 Rewrite product_sx_eq; Auto.
  Do 2 Rewrite product_dx_eq; Auto.
Qed.

Definition product_isom_inv [p,q:Product] : (Inv (product_isom p q)).
Proof.
  Intros; Split with (product_isom q p).
  Abstract Split; Unfold is_inv_sx is_inv_dx; Apply product_isom_eq.
Defined.

End Product.

Definition has_product [A:Cat] : Type := (x,y:A)(Product x y).

Section Product_Comm.

Variable A:Cat; x,y:A.
Variable p:(Product x y); q:(Product y x).

Definition product_comm : (mor p q) := (product q (proj2 p) (proj1 p)).

Local h : (mor q p) := (product p (proj2 q) (proj1 q)).

Definition product_comm_inv : (Inv product_comm).
Proof.
  Split with h.
  Abstract Split; Unfold product_comm h is_inv_sx is_inv_dx;
    Apply product_f_eq_g; Rewrite oo_assoc;
    Repeat (Rewrite product_sx_eq Orelse Rewrite product_dx_eq); Auto.
Defined.

End Product_Comm.

Section Product_Assoc.

Variable A:Cat; x,y,z:A.
Variable p:(Product y z); s:(Product x p).
Variable q:(Product x y); t:(Product q z).

Definition product_assoc : (mor s t) :=
 (product t (product q (proj1 s) (oo (proj1 p) (proj2 s)))
   (oo (proj2 p) (proj2 s))).

Local h : (mor t s) :=
 (product s (oo (proj1 q) (proj1 t))
   (product p (oo (proj2 q) (proj1 t)) (proj2 t))).

Definition product_assoc_inv : (Inv product_assoc).
Proof.
  Split with h.
  Let rew1 = (Rewrite product_dx_eq Orelse Rewrite product_sx_eq) In
  Let rew2 = (Rewrite oo_assoc; rew1) In
  Let rew3 = (Rewrite <- oo_assoc; rew1) In
  Let rew = (Repeat (rew1 Orelse rew2 Orelse rew3)) In
  Abstract Split; Unfold product_assoc h is_inv_sx is_inv_dx;
    Repeat (rew Orelse Apply product_f_eq_g); Auto.
Defined.

End Product_Assoc.

End Product.