Library UniMath.Ktheory.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.Ktheory.Representation
        UniMath.Ktheory.Utilities
        UniMath.Ktheory.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).