theorem KLRW.implicit_rel_eq_rel {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] {f g : KLRWFreeAlg R parameters} (h : KLRWImplicitConRel f g) : (KLRWRel R parameters) f g

theorem KLRW.explicit_rel_eq_rel {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] {f g : KLRWFreeAlg R parameters} (h : KLRWExplicitConRel f g) : (KLRWRel R parameters) f g

theorem KLRW.rel_eq_same_con_class {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] {x y : KLRWFreeAlg R parameters} (h : (KLRWRel R parameters) x y) : (KLRWRel R parameters).mk' x = (KLRWRel R parameters).mk' y

theorem KLRW.idem_is_idem {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) : idem_morph R M * idem_morph R M = idem_morph R M

theorem KLRW.id_mul_left {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] {X Y : KLRWObject parameters} (f : KLRWAlg R parameters) (hf : f ∈ KLRWHom R X Y) : idem_morph R Y * f = f

theorem KLRW.id_mul_right {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] {X Y : KLRWObject parameters} (f : KLRWAlg R parameters) (hf : f ∈ KLRWHom R X Y) : f * idem_morph R X = f

theorem KLRW.mem_KLRWHom_iff {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] {X Y : KLRWObject parameters} (f : KLRWAlg R parameters) : f ∈ KLRWHom R X Y ↔ idem_morph R Y * f * idem_morph R X = f

theorem KLRW.KLRWHom_comp_mem {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] {X Y Z : KLRWObject parameters} {f g : KLRWAlg R parameters} (hf : f ∈ KLRWHom R X Y) (hg : g ∈ KLRWHom R Y Z) : g * f ∈ KLRWHom R X Z

structure KLRW.KLRWObject.WithRing {V : Type u_1} [DecidableEq V] [Fintype V] (R : Type u_3) [CommRing R] (parameters : KLRWStructure V) : Type u_1

• obj : KLRWObject parameters

@[implicit_reducible]

noncomputable instance KLRW.instCategoryWithRing {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] : CategoryTheory.Category.{max u_1 u_2, u_1} (KLRWObject.WithRing R parameters)

Equations

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

theorem KLRW.KLRWHom.ext {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] {X Y : KLRWObject.WithRing R parameters} {f g : X ⟶ Y} (h : ↑f = ↑g) : f = g

theorem KLRW.KLRWHom.ext_iff {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] {X Y : KLRWObject.WithRing R parameters} {f g : X ⟶ Y} : f = g ↔ ↑f = ↑g

@[implicit_reducible]

noncomputable instance KLRW.instPreadditiveWithRing {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] : CategoryTheory.Preadditive (KLRWObject.WithRing R parameters)

Equations

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

@[implicit_reducible]

noncomputable instance KLRW.instLinearWithRing {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] : CategoryTheory.Linear R (KLRWObject.WithRing R parameters)

Equations

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