Library UniMath.CategoryTheory.RepresentableFunctors.RawMatrix

raw matrices

Raw matrices of a map are formed from a product decomposition of the target or from a sum decomposition of the source. We call them "raw" to distinguish them from matrices formed from direct sum decompositions.

Require Import
        UniMath.Foundations.Sets
        UniMath.CategoryTheory.Core.Categories
        UniMath.CategoryTheory.Core.Isos
        UniMath.CategoryTheory.Core.Functors
        UniMath.CategoryTheory.Core.NaturalTransformations
        UniMath.CategoryTheory.RepresentableFunctors.Representation
        UniMath.CategoryTheory.RepresentableFunctors.Precategories.
Local Open Scope cat.

Definition to_row {C:category} {I} {b:I -> ob C}
           (B:Sum b) {d:ob C} :
  (Hom C (universalObject B) d ) ≃ (∏ j , Hom C (b j) d ).
Show proof.

intros. exact (universalProperty B d).

Definition from_row {C:category} {I} {b:I -> ob C}
(B:Sum b) {d:ob C} :
(∏ j , Hom C (b j) d ) ≃ (Hom C (universalObject B) d ).
Show proof.

intros. apply invweq. apply to_row.

Lemma from_row_entry {C:category} {I} {b:I -> ob C}
(B:Sum b) {d:ob C} (f : ∏ j , Hom C (b j) d) :
∏ j , from_row B f ∘ opp_mor (universalElement B j) = f j.
Show proof.

intros. exact (eqtohomot (homotweqinvweq (to_row B) f) j).

Definition to_col {C:category} {I} {d:I -> ob C} (D:Product d) {b:ob C} :
(Hom C b (universalObject D)) ≃ (∏ i , Hom C b (d i)).
Show proof.

intros. exact (universalProperty D b).

Definition from_col {C:category} {I} {d:I -> ob C}
(D:Product d) {b:ob C} :
(∏ i , Hom C b (d i)) ≃ (Hom C b (universalObject D)).
Show proof.

intros. apply invweq. apply to_col.

Lemma from_col_entry {C:category} {I} {b:I -> ob C}
(D:Product b) {d:ob C} (f : ∏ i , Hom C d (b i)) :
∏ i , universalElement D i ∘ from_col D f = f i.
Show proof.

intros.
apply (eqtohomot (homotweqinvweq (to_col D) f ) i).

Definition to_matrix {C:category}
           {I} {d:I -> ob C} (D:Product d)
           {J} {b:J -> ob C} (B:Sum b) :
  (Hom C (universalObject B) (universalObject D))
    ≃
    (∏ i j , Hom C (b j) (d i)).
Show proof.

  intros. apply @weqcomp with (Y := ∏ i , Hom C (universalObject B) (d i)).
  { apply to_col. }
  { apply weqonsecfibers; intro i. apply to_row. }

Definition from_matrix {C:category}
           {I} {d:I -> ob C} (D:Product d)
           {J} {b:J -> ob C} (B:Sum b) :
           weq (∏ i j , Hom C (b j) (d i)) (Hom C (universalObject B) (universalObject D)).
Show proof.

intros. apply invweq. apply to_matrix.

Lemma from_matrix_entry {C:category}
           {I} {d:I -> ob C} (D:Product d)
           {J} {b:J -> ob C} (B:Sum b)
           (f : ∏ i j , Hom C (b j) (d i)) :
  ∏ i j , (universalElement D i ∘ from_matrix D B f ) ∘ opp_mor (universalElement B j) = f i j.
Show proof.

intros. exact (eqtohomot (eqtohomot (homotweqinvweq (to_matrix D B) f) i) j).

Lemma from_matrix_entry_assoc {C:category}
           {I} {d:I -> ob C} (D:Product d)
           {J} {b:J -> ob C} (B:Sum b)
           (f : ∏ i j , Hom C (b j) (d i)) :
  ∏ i j , universalElement D i ∘ (from_matrix D B f ∘ opp_mor(universalElement B j)) = f i j.
Show proof.

intros. rewrite <- assoc. exact (from_matrix_entry D B f i j).