structure CMat_ (C : Type u_1) : Type u_1

• ofList :: (
• toList : List C
• )

@[implicit_reducible]

instance instTexifyCMat_ (C : Type u_1) [Texify C] : Texify (CMat_ C)

Equations

• One or more equations did not get rendered due to their size.

def «term[_,]ₘ» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem CMat_.toList_empty {C : Type u_1} : { toList := [] }.toList = []

theorem CMat_.toList_singleton {C : Type u_1} (A : C) : { toList := [A] }.toList = [A]

@[irreducible]

def CMat_.ι {C : Type u_1} (M : CMat_ C) : Type

Mirrors the API of CategoryTheory.Mat_.ι. This is irreducible because it is effectively irreducible in Mat_, and we should mirror the API.

Equations

• M.ι = Fin M.toList.length

def CMat_.ι.toFin {C : Type u_1} {M : CMat_ C} (i : M.ι) : Fin M.toList.length

Equations

• i.toFin = i

def CMat_.ι.ofFin {C : Type u_1} {M : CMat_ C} (i : Fin M.toList.length) : M.ι

Equations

• CMat_.ι.ofFin i = i

@[simp]

theorem CMat_.ι.ofFin_toFin {C : Type u_1} {M : CMat_ C} (i : M.ι) : ofFin i.toFin = i

@[simp]

theorem CMat_.ι.toFin_ofFin {C : Type u_1} {M : CMat_ C} (i : Fin M.toList.length) : (ofFin i).toFin = i

def CMat_.ι.finEquiv {C : Type u_1} {M : CMat_ C} : M.ι ≃ Fin M.toList.length

Equations

• CMat_.ι.finEquiv = { toFun := CMat_.ι.toFin, invFun := CMat_.ι.ofFin, left_inv := ⋯, right_inv := ⋯ }

@[implicit_reducible]

instance CMat_.fintype {C : Type u_1} {M : CMat_ C} : Fintype M.ι

Equations

• CMat_.fintype = { elems := CMat_.fintype._aux_1, complete := ⋯ }

@[implicit_reducible]

instance CMat_.instDecidableEqι {C : Type u_1} {M : CMat_ C} : DecidableEq M.ι

Equations

• CMat_.instDecidableEqι = CMat_.instDecidableEqι._aux_1

@[irreducible]

def CMat_.X {C : Type u_1} {M : CMat_ C} : M.ι → C

Mirrors the API of CategoryTheory.Mat_.X

Equations

• CMat_.X i = M.toList[i.toFin]

def CMat_.Hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (M N : CMat_ C) : Type u_2

Mirrors the API of CategoryTheory.Mat_.Hom

Equations

• M.Hom N = DMatrix M.ι N.ι fun (i : M.ι) (j : N.ι) => CMat_.X i ⟶ CMat_.X j

def CMat_.Hom.id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (M : CMat_ C) : M.Hom M

Mirrors the API of CategoryTheory.Mat_.Hom.id

Equations

• CMat_.Hom.id M i j = if h : i = j then CategoryTheory.eqToHom ⋯ else 0

def CMat_.Hom.comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {M N K : CMat_ C} (f : M.Hom N) (g : N.Hom K) : M.Hom K

Mirrors the API of CategoryTheory.Mat_.Hom.comp

Equations

• f.comp g i k = ∑ j : N.ι, CategoryTheory.CategoryStruct.comp (f i j) (g j k)

@[implicit_reducible]

instance CMat_.instCategory {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : CategoryTheory.Category.{u_2, u_1} (CMat_ C)

Equations

• CMat_.instCategory = { Hom := CMat_.Hom, id := CMat_.Hom.id, comp := fun {X Y Z : CMat_ C} (f : X.Hom Y) (g : Y.Hom Z) => f.comp g, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

@[implicit_reducible]

instance CMat_.instTexifyHomOfHom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [(X Y : C) → Texify (X ⟶ Y)] (M N : CMat_ C) : Texify (M.Hom N)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance CMat_.instTexifyHom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [(X Y : C) → Texify (X ⟶ Y)] (M N : CMat_ C) : Texify (M ⟶ N)

Equations

• One or more equations did not get rendered due to their size.

def CMat_.Hom.ofFin {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] (xs ys : List C) (f : (i : Fin xs.length) → (j : Fin ys.length) → xs[i] ⟶ ys[j]) : { toList := xs } ⟶ { toList := ys }

Constructor for explicit morphisms, e.g. in interactive use

Equations

• CMat_.Hom.ofFin xs ys f = f

theorem CMat_.hom_ext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {M N : CMat_ C} (f g : M ⟶ N) (H : ∀ (i : M.ι) (j : N.ι), f i j = g i j) : f = g

theorem CMat_.hom_ext_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {M N : CMat_ C} {f g : M ⟶ N} : f = g ↔ ∀ (i : M.ι) (j : N.ι), f i j = g i j

theorem CMat_.id_def {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (M : CMat_ C) : CategoryTheory.CategoryStruct.id M = fun (i j : M.ι) => if h : i = j then CategoryTheory.eqToHom ⋯ else 0

theorem CMat_.id_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (M : CMat_ C) (i j : M.ι) : CategoryTheory.CategoryStruct.id M i j = if h : i = j then CategoryTheory.eqToHom ⋯ else 0

@[simp]

theorem CMat_.id_apply_self {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (M : CMat_ C) (i : M.ι) : CategoryTheory.CategoryStruct.id M i i = CategoryTheory.CategoryStruct.id (X i)

@[simp]

theorem CMat_.id_apply_of_ne {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (M : CMat_ C) (i j : M.ι) (h : i ≠ j) : CategoryTheory.CategoryStruct.id M i j = 0

theorem CMat_.comp_def {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {M N K : CMat_ C} (f : M ⟶ N) (g : N ⟶ K) : CategoryTheory.CategoryStruct.comp f g = fun (i : M.ι) (k : K.ι) => ∑ j : N.ι, CategoryTheory.CategoryStruct.comp (f i j) (g j k)

@[simp]

theorem CMat_.comp_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {M N K : CMat_ C} (f : M ⟶ N) (g : N ⟶ K) (i : M.ι) (k : K.ι) : CategoryTheory.CategoryStruct.comp f g i k = ∑ j : N.ι, CategoryTheory.CategoryStruct.comp (f i j) (g j k)

@[implicit_reducible]

instance CMat_.instInhabitedHom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (M N : CMat_ C) : Inhabited (M ⟶ N)

Equations

• M.instInhabitedHom N = { default := fun (i : M.ι) (j : N.ι) => 0 }

@[implicit_reducible]

instance CMat_.instAddCommGroupHom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (M N : CMat_ C) : AddCommGroup (M ⟶ N)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CMat_.add_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {M N : CMat_ C} (f g : M ⟶ N) (i : M.ι) (j : N.ι) : (f + g) i j = f i j + g i j

@[implicit_reducible]

instance CMat_.instPreadditive {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : CategoryTheory.Preadditive (CMat_ C)

Equations

• CMat_.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }

def CMat_.cbiprod {C : Type u_1} (M N : CMat_ C) : CMat_ C

Equations

• M.cbiprod N = { toList := M.toList ++ N.toList }

def CMat_.cbiprod_ι_equiv' {C : Type u_1} {M N : CMat_ C} : (M.cbiprod N).ι ≃ M.ι ⊕ N.ι

Equations

• CMat_.cbiprod_ι_equiv' = ((CMat_.ι.finEquiv.trans (finCongr ⋯)).trans finSumFinEquiv.symm).trans (CMat_.ι.finEquiv.symm.sumCongr CMat_.ι.finEquiv.symm)

theorem CMat_.X_symm_cbiprod_ι_equiv'_inl {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (M N : CMat_ C) (i : M.ι) : X (cbiprod_ι_equiv'.symm (Sum.inl i)) = X i

theorem CMat_.X_symm_cbiprod_ι_equiv'_inr {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (M N : CMat_ C) (i : N.ι) : X (cbiprod_ι_equiv'.symm (Sum.inr i)) = X i

@[implicit_reducible]

instance CMat_.instComputableBinaryBiproduct {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : ComputableBinaryBiproduct (CMat_ C)

Equations

• One or more equations did not get rendered due to their size.

def CMat_.cbiprod_ι_equiv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {M N : CMat_ C} : (M ⊞ᶜ N).ι ≃ M.ι ⊕ N.ι

Same as cbiprod_ι_equiv but expressed with proper notation and thus with types

Equations

• CMat_.cbiprod_ι_equiv = CMat_.cbiprod_ι_equiv'

instance CMat_.instIsEmptyιOfListNil {C : Type u_1} : IsEmpty { toList := [] }.ι

theorem CMat_.hom_from_empty_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (M : CMat_ C) (h : { toList := [] } ⟶ M) : h = 0

theorem CMat_.hom_to_empty_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (M : CMat_ C) (h : M ⟶ { toList := [] }) : h = 0

@[implicit_reducible]

instance CMat_.instHasExplicitZeroObject {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : HasExplicitZeroObject (CMat_ C)

Equations

• CMat_.instHasExplicitZeroObject = HasExplicitZeroObject.mkOfPreadditive (CMat_ C) { toList := [] } ⋯ ⋯

@[implicit_reducible]

instance CMat_.instDecidablePredIsZero {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Preadditive V] [DecidablePred CategoryTheory.Limits.IsZero] : DecidablePred CategoryTheory.Limits.IsZero

Equations

• M.instDecidablePredIsZero = if h : (M.toList.all fun (x : V) => decide (CategoryTheory.Limits.IsZero x)) = true then isTrue ⋯ else isFalse ⋯

def CMat_.toMat_ (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor (CMat_ C) (CategoryTheory.Mat_ C)

Equations

• CMat_.toMat_ C = { obj := fun (M : CMat_ C) => { ι := M.ι, fintype := CMat_.fintype, X := CMat_.X }, map := fun {X Y : CMat_ C} (f : X ⟶ Y) => f, map_id := ⋯, map_comp := ⋯ }

instance CMat_.instFaithfulMat_ToMat_ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : (toMat_ C).Faithful

instance CMat_.instFullMat_ToMat_ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : (toMat_ C).Full

noncomputable def CMat_.ofMat_ {C : Type u_1} (M' : CategoryTheory.Mat_ C) : CMat_ C

Given a Mat_ object M', construct the corresponding CMat_ object.

Equations

• CMat_.ofMat_ M' = { toList := List.ofFn (M'.X ∘ ⇑(Fintype.equivFin M'.ι).symm) }

instance CMat_.instEssSurjMat_ToMat_ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : (toMat_ C).EssSurj

instance CMat_.instIsEquivalenceMat_ToMat_ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : (toMat_ C).IsEquivalence

theorem CMat_.apply_X_ofList_singleton (C : Type u_1) {A : C} (i : { toList := [A] }.ι) : X i = A

This is not a simp lemma because I am worried that this is often an equality of types. But I think this could work as a simp lemma, I'm just not sure if it would cause defeq issues.

theorem CMat_.singleton_ι_card (C : Type u_1) {A : C} : Fintype.card { toList := [A] }.ι = 1

@[implicit_reducible]

instance CMat_.singleton_ι_unique (C : Type u_1) {A : C} : Unique { toList := [A] }.ι

Equations

• CMat_.singleton_ι_unique C = { default := CMat_.singleton_ι_unique._aux_1 C, uniq := ⋯ }

def CMat_.embedding (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor C (CMat_ C)

Equations

• CMat_.embedding C = { obj := fun (X : C) => { toList := [X] }, map := fun {A B : C} (f : A ⟶ B) (i : { toList := [A] }.ι) (j : { toList := [B] }.ι) => cast ⋯ f, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CMat_.ofList_singleton (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {A : C} : { toList := [A] } = (embedding C).obj A

@[simp]

theorem CMat_.toList_embedding (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {A : C} : ((embedding C).obj A).toList = [A]

theorem CMat_.X_embedding (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {A : C} (i : ((embedding C).obj A).ι) : X i = A

@[implicit_reducible]

instance CMat_.instUniqueιObjEmbedding (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {A : C} : Unique ((embedding C).obj A).ι

Equations

• CMat_.instUniqueιObjEmbedding C = CMat_.singleton_ι_unique C

def CMat_.Embedding.fullyFaithful (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : (embedding C).FullyFaithful

Equations

• One or more equations did not get rendered due to their size.

instance CMat_.Embedding.instFaithfulEmbedding (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : (embedding C).Faithful

instance CMat_.Embedding.instFullEmbedding (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : (embedding C).Full

instance CMat_.Embedding.instAdditiveEmbedding (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : (embedding C).Additive

def CMat_.extend {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive D] [ComputableBinaryBiproduct D] [HasExplicitZeroObject D] (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.Functor (CMat_ C) D

Equations

• CMat_.extend F = { obj := fun (M : CMat_ C) => (List.map F.obj M.toList).cbiprod, map := fun {M N : CMat_ C} (f : M ⟶ N) => sorry, map_id := ⋯, map_comp := ⋯ }

def CMat_.bind {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor (CMat_ (CMat_ C)) (CMat_ C)

Equations

• CMat_.bind = CMat_.extend (CategoryTheory.Functor.id (CMat_ C))

def CMat_.mapCMat_ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.Functor (CMat_ C) (CMat_ D)

Equations

• CMat_.mapCMat_ F = CMat_.extend (F.comp (CMat_.embedding D))

@[implicit_reducible]

instance CMat_.instModuleDMatrix {R : Type u_1} [Semiring R] (m : Type u_2) (n : Type u_3) (α : m → n → Type u_4) [(i : m) → (j : n) → AddCommGroup (α i j)] [(i : m) → (j : n) → Module R (α i j)] : Module R (DMatrix m n α)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance CMat_.instLinear {R : Type u_1} [Semiring R] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] : CategoryTheory.Linear R (CMat_ C)

Equations

• One or more equations did not get rendered due to their size.