Schlessinger.Categories.VectorSpace

theorem vs.isZero_zero {R : Type u} [CommRing R] :

CategoryTheory.Limits.IsZero (FGModuleCat.of R PUnit.{u_1 + 1})

instance vs.instHasZeroObjectFGModuleCat_schlessinger {R : Type u} [CommRing R] :

CategoryTheory.Limits.HasZeroObject (FGModuleCat R)

noncomputable def vs.isTerminalObjZero {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts L] :

CategoryTheory.Limits.IsTerminal (L.obj 0)

Equations

vs.isTerminalObjZero L = CategoryTheory.Limits.IsTerminal.isTerminalObj L 0 CategoryTheory.Limits.HasZeroObject.zeroIsTerminal

Instances For

source

noncomputable instance vs.instUniqueObjFGModuleCatOfNat_schlessinger {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts L] :

Unique (L.obj 0)

Equations

vs.instUniqueObjFGModuleCatOfNat_schlessinger L = (CategoryTheory.Limits.Types.isTerminalEquivUnique (L.obj 0)) (vs.isTerminalObjZero L)

source

@[reducible, inline]

abbrev vs.prod {R : Type u} [CommRing R] (M N : FGModuleCat R) :

FGModuleCat R

Equations

vs.prod M N = FGModuleCat.of R (↑M × ↑N)

Instances For

source

def vs.fst {R : Type u} [CommRing R] (M N : FGModuleCat R) :

FGModuleCat.of R (↑M × ↑N) ⟶ FGModuleCat.of R ↑M

Equations

vs.fst M N = FGModuleCat.ofHom (LinearMap.fst R ↑M ↑N)

Instances For

source

def vs.snd {R : Type u} [CommRing R] (M N : FGModuleCat R) :

FGModuleCat.of R (↑M × ↑N) ⟶ FGModuleCat.of R ↑N

Equations

vs.snd M N = FGModuleCat.ofHom (LinearMap.snd R ↑M ↑N)

Instances For

source

def vs.lift {R : Type u} [CommRing R] {M N M' : FGModuleCat R} (f : M' ⟶ M) (g : M' ⟶ N) :

FGModuleCat.of R ↑M'.obj ⟶ FGModuleCat.of R (↑M.obj × ↑N.obj)

Equations

vs.lift f g = FGModuleCat.ofHom ((ModuleCat.Hom.hom f).prod (ModuleCat.Hom.hom g))

Instances For

source

def vs.map {R : Type u} [CommRing R] {M N M' N' : FGModuleCat R} (f : M' ⟶ M) (g : N' ⟶ N) :

FGModuleCat.of R (↑M'.obj × ↑N'.obj) ⟶ FGModuleCat.of R (↑M.obj × ↑N.obj)

Equations

vs.map f g = FGModuleCat.ofHom ((ModuleCat.Hom.hom f).prodMap (ModuleCat.Hom.hom g))

Instances For

source

def vs.diag {R : Type u} [CommRing R] (M : FGModuleCat R) :

FGModuleCat.of R ↑M.obj ⟶ FGModuleCat.of R (↑M.obj × ↑M.obj)

Equations

vs.diag M = vs.lift (CategoryTheory.CategoryStruct.id M) (CategoryTheory.CategoryStruct.id M)

Instances For

source

@[simp]

theorem vs.lift_fst {R : Type u} [CommRing R] (M N : FGModuleCat R) {M' : FGModuleCat R} (f : M' ⟶ M) (g : M' ⟶ N) :

CategoryTheory.CategoryStruct.comp (lift f g) (fst M N) = f

source

@[simp]

theorem vs.lift_snd {R : Type u} [CommRing R] (M N : FGModuleCat R) {M' : FGModuleCat R} (f : M' ⟶ M) (g : M' ⟶ N) :

CategoryTheory.CategoryStruct.comp (lift f g) (snd M N) = g

source

@[simp]

theorem vs.map_fst {R : Type u} [CommRing R] (M N : FGModuleCat R) {M' N' : FGModuleCat R} (f : M' ⟶ M) (g : N' ⟶ N) :

CategoryTheory.CategoryStruct.comp (map f g) (fst M N) = CategoryTheory.CategoryStruct.comp (fst M' N') f

source

@[simp]

theorem vs.map_snd {R : Type u} [CommRing R] (M N : FGModuleCat R) {M' N' : FGModuleCat R} (f : M' ⟶ M) (g : N' ⟶ N) :

CategoryTheory.CategoryStruct.comp (map f g) (snd M N) = CategoryTheory.CategoryStruct.comp (snd M' N') g

source

noncomputable def vs.cone {R : Type u} [CommRing R] (M N : FGModuleCat R) :

CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair M N)

Equations

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

Instances For

source

@[simp]

theorem vs.cone_cone_pt_obj_isAddCommGroup_sub {R : Type u} [CommRing R] (M N : FGModuleCat R) (p q : ↑M × ↑N) :

p - q = (p.1 - q.1, p.2 - q.2)

source

@[simp]

theorem vs.cone_cone_pt_obj_isAddCommGroup_zero {R : Type u} [CommRing R] (M N : FGModuleCat R) :

0 = (0, 0)

source

@[simp]

theorem vs.cone_cone_pt_obj_isModule_smul {R : Type u} [CommRing R] (M N : FGModuleCat R) (a : R) (p : ↑M × ↑N) :

SMul.smul a p = (a • p.1, a • p.2)

source

@[simp]

theorem vs.cone_cone_pt_obj_carrier {R : Type u} [CommRing R] (M N : FGModuleCat R) :

↑(cone M N).cone.pt.obj = (↑M × ↑N)

source

@[simp]

theorem vs.cone_cone_pt_obj_isAddCommGroup_add {R : Type u} [CommRing R] (M N : FGModuleCat R) (p q : ↑M × ↑N) :

p + q = (p.1 + q.1, p.2 + q.2)

source

@[simp]

theorem vs.cone_cone_pt_obj_isAddCommGroup_neg {R : Type u} [CommRing R] (M N : FGModuleCat R) (p : ↑M × ↑N) :

-p = (-p.1, -p.2)

source

@[simp]

theorem vs.cone_cone_π_app {R : Type u} [CommRing R] (M N : FGModuleCat R) (j : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) :

(cone M N).cone.π.app j = CategoryTheory.Limits.WalkingPair.rec (fst M N) (snd M N) j.as

source

@[simp]

theorem vs.cone_cone_pt_obj_isAddCommGroup_zsmul {R : Type u} [CommRing R] (M N : FGModuleCat R) (z : ℤ) (a : ↑M × ↑N) :

z • a = (z • a.1, z • a.2)

source

@[simp]

theorem vs.cone_cone_pt_obj_isAddCommGroup_nsmul {R : Type u} [CommRing R] (M N : FGModuleCat R) (z : ℕ) (a : ↑M × ↑N) :

z • a = (z • a.1, z • a.2)

source

@[simp]

theorem vs.cone_isLimit_lift_hom_apply {R : Type u} [CommRing R] (M N : FGModuleCat R) (s : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair M N)) (i : ↑s.1.obj) :

(ModuleCat.Hom.hom ((cone M N).isLimit.lift s)) i = ((ModuleCat.Hom.hom (CategoryTheory.Limits.BinaryFan.fst s)) i, (ModuleCat.Hom.hom (CategoryTheory.Limits.BinaryFan.snd s)) i)

source

theorem vs.cone_π_left {R : Type u} [CommRing R] (M N : FGModuleCat R) :

(cone M N).cone.π.app { as := CategoryTheory.Limits.WalkingPair.left } = fst M N

source

theorem vs.cone_π_right {R : Type u} [CommRing R] (M N : FGModuleCat R) :

(cone M N).cone.π.app { as := CategoryTheory.Limits.WalkingPair.right } = snd M N

source

def vs.swap {R : Type u} [CommRing R] (M N : FGModuleCat R) :

prod M N ≅ prod N M

Equations

vs.swap M N = (LinearEquiv.prodComm R ↑M ↑N).toFGModuleCatIso

Instances For

source

@[simp]

theorem vs.swap_hom_fst {R : Type u} [CommRing R] (M N : FGModuleCat R) :

CategoryTheory.CategoryStruct.comp (swap M N).hom (fst N M) = snd M N

source

@[simp]

theorem vs.swap_hom_snd {R : Type u} [CommRing R] (M N : FGModuleCat R) :

CategoryTheory.CategoryStruct.comp (swap M N).hom (snd N M) = fst M N

source

def vs.assoc {R : Type u} [CommRing R] (M N P : FGModuleCat R) :

prod (prod M N) P ≅ prod M (prod N P)

Equations

vs.assoc M N P = (LinearEquiv.prodAssoc R ↑M ↑N ↑P).toFGModuleCatIso

Instances For

source

@[simp]

theorem vs.assoc_fst {R : Type u} [CommRing R] (M N P : FGModuleCat R) :

CategoryTheory.CategoryStruct.comp (assoc M N P).hom (fst M (prod N P)) = CategoryTheory.CategoryStruct.comp (fst (prod M N) P) (fst M N)

source

@[simp]

theorem vs.assoc_snd_fst {R : Type u} [CommRing R] (M N P : FGModuleCat R) :

CategoryTheory.CategoryStruct.comp (assoc M N P).hom (CategoryTheory.CategoryStruct.comp (snd M (prod N P)) (fst N P)) = CategoryTheory.CategoryStruct.comp (fst (prod M N) P) (snd M N)

source

@[simp]

theorem vs.assoc_snd_snd {R : Type u} [CommRing R] (M N P : FGModuleCat R) :

CategoryTheory.CategoryStruct.comp (assoc M N P).hom (CategoryTheory.CategoryStruct.comp (snd M (prod N P)) (snd N P)) = snd (prod M N) P

source

def vs.inl {R : Type u} [CommRing R] (M N : FGModuleCat R) :

FGModuleCat.of R ↑M ⟶ FGModuleCat.of R (↑M × ↑N)

Equations

vs.inl M N = FGModuleCat.ofHom (LinearMap.inl R ↑M ↑N)

Instances For

source

@[simp]

theorem vs.inl_fst {R : Type u} [CommRing R] (M N : FGModuleCat R) :

CategoryTheory.CategoryStruct.comp (inl M N) (fst M N) = CategoryTheory.CategoryStruct.id (FGModuleCat.of R ↑M)

source

@[simp]

theorem vs.inl_snd {R : Type u} [CommRing R] (M N : FGModuleCat R) :

CategoryTheory.CategoryStruct.comp (inl M N) (snd M N) = 0

source

def vs.inr {R : Type u} [CommRing R] (M N : FGModuleCat R) :

FGModuleCat.of R ↑N ⟶ FGModuleCat.of R (↑M × ↑N)

Equations

vs.inr M N = FGModuleCat.ofHom (LinearMap.inr R ↑M ↑N)

Instances For

source

@[simp]

theorem vs.inr_fst {R : Type u} [CommRing R] (M N : FGModuleCat R) :

CategoryTheory.CategoryStruct.comp (inr M N) (snd M N) = CategoryTheory.CategoryStruct.id (FGModuleCat.of R ↑N)

source

@[simp]

theorem vs.inr_snd {R : Type u} [CommRing R] (M N : FGModuleCat R) :

CategoryTheory.CategoryStruct.comp (inr M N) (fst M N) = 0

source

def vs.smul_hom {R : Type u} [CommRing R] (M : FGModuleCat R) (a : R) :

FGModuleCat.of R ↑M ⟶ FGModuleCat.of R ↑M

Equations

vs.smul_hom M a = FGModuleCat.ofHom (DistribMulAction.toLinearMap R (↑M) a)

Instances For

source

@[simp]

theorem vs.smul_hom_hom_apply {R : Type u} [CommRing R] (M : FGModuleCat R) (a : R) (a✝ : ↑M) :

(ModuleCat.Hom.hom (smul_hom M a)) a✝ = a • a✝

source

@[simp]

theorem vs.smul_hom_one {R : Type u} [CommRing R] (M : FGModuleCat R) :

smul_hom M 1 = CategoryTheory.CategoryStruct.id M

source

@[simp]

theorem vs.smul_hom_zero {R : Type u} [CommRing R] (M : FGModuleCat R) :

smul_hom M 0 = 0

source

def vs.add_hom {R : Type u} [CommRing R] (M : FGModuleCat R) :

FGModuleCat.of R (↑M × ↑M) ⟶ FGModuleCat.of R ↑M

Equations

vs.add_hom M = FGModuleCat.ofHom (LinearMap.id.coprod LinearMap.id)

Instances For

source

@[simp]

theorem vs.add_hom_hom_apply {R : Type u} [CommRing R] (M : FGModuleCat R) (a : ↑M × ↑M) :

(ModuleCat.Hom.hom (add_hom M)) a = a.1 + a.2

source

def vs.zero_hom {R : Type u} [CommRing R] (M N : FGModuleCat R) :

M ⟶ N

Equations

vs.zero_hom M N = 0

Instances For

source

@[simp]

theorem vs.zero_hom_hom_apply {R : Type u} [CommRing R] (M N : FGModuleCat R) (a✝ : ↑M.obj) :

(ModuleCat.Hom.hom (zero_hom M N)) a✝ = 0

source

noncomputable def vs.islimit_map {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] :

CategoryTheory.Limits.IsLimit ((CategoryTheory.Limits.Cones.postcompose (CategoryTheory.Limits.pairComp M N L).hom).obj (L.mapCone (cone M N).cone))

Equations

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

Instances For

source

noncomputable def vs.iso {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] :

L.obj (prod M N) ≅ L.obj M × L.obj N

Equations

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

Instances For

source

theorem vs.iso_hom_fst {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] :

L.map (fst M N) = CategoryTheory.CategoryStruct.comp (iso L M N).hom (CategoryTheory.Limits.Types.binaryProductCone (L.obj M) (L.obj N)).fst

source

theorem vs.iso_inv_fst {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] :

CategoryTheory.CategoryStruct.comp (iso L M N).inv (L.map (fst M N)) = (CategoryTheory.Limits.Types.binaryProductCone (L.obj M) (L.obj N)).fst

source

@[simp]

theorem vs.iso_inv_fst_apply {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] (x : L.obj M × L.obj N) :

L.map (fst M N) ((iso L M N).inv x) = x.1

source

theorem vs.iso_hom_fst_apply {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] (x : L.obj (prod M N)) :

L.map (fst M N) x = ((iso L M N).hom x).1

source

theorem vs.iso_hom_snd {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] :

L.map (snd M N) = CategoryTheory.CategoryStruct.comp (iso L M N).hom (CategoryTheory.Limits.Types.binaryProductCone (L.obj M) (L.obj N)).snd

source

theorem vs.iso_inv_snd {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] :

CategoryTheory.CategoryStruct.comp (iso L M N).inv (L.map (snd M N)) = (CategoryTheory.Limits.Types.binaryProductCone (L.obj M) (L.obj N)).snd

source

@[simp]

theorem vs.iso_inv_snd_apply {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] (x : L.obj M × L.obj N) :

L.map (snd M N) ((iso L M N).inv x) = x.2

source

theorem vs.iso_hom_snd_apply {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] (x : L.obj (prod M N)) :

L.map (snd M N) x = ((iso L M N).hom x).2

source

theorem vs.iso_map {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] (M' N' : FGModuleCat R) (x : L.obj M) (y : L.obj N) (f : M ⟶ M') (g : N ⟶ N') :

(iso L M' N').inv (L.map f x, L.map g y) = L.map (map f g) ((iso L M N).inv (x, y))

source

theorem vs.iso_map_1 {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] (M' : FGModuleCat R) (x : L.obj M) (y : L.obj N) (f : M ⟶ M') :

(iso L M' N).inv (L.map f x, y) = L.map (map f (CategoryTheory.CategoryStruct.id N)) ((iso L M N).inv (x, y))

source

theorem vs.iso_map_2 {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] (N' : FGModuleCat R) (x : L.obj M) (y : L.obj N) (g : N ⟶ N') :

(iso L M N').inv (x, L.map g y) = L.map (map (CategoryTheory.CategoryStruct.id M) g) ((iso L M N).inv (x, y))

source

instance vs.instSMulObjFGModuleCat_schlessinger {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M : FGModuleCat R) :

SMul R (L.obj M)

Equations

vs.instSMulObjFGModuleCat_schlessinger L M = { smul := fun (r : R) (x : L.obj M) => L.map (vs.smul_hom M r) x }

source

theorem vs.smul_def {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M : FGModuleCat R) (a : R) (x : L.obj M) :

a • x = L.map (smul_hom M a) x

source

noncomputable instance vs.instZeroObjFGModuleCat_schlessinger {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] :

Zero (L.obj M)

Equations

vs.instZeroObjFGModuleCat_schlessinger L M = { zero := L.map (vs.zero_hom 0 M) default }

source

theorem vs.zero_def {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] :

0 = L.map (zero_hom 0 M) default

source

noncomputable instance vs.instAddObjFGModuleCat_schlessinger {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] :

Add (L.obj M)

Equations

vs.instAddObjFGModuleCat_schlessinger L M = { add := fun (x y : L.obj M) => L.map (vs.add_hom M) ((vs.iso L M M).inv (x, y)) }

source

theorem vs.add_def {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] (x y : L.obj M) :

x + y = L.map (add_hom M) ((iso L M M).inv (x, y))

source

@[simp]

theorem vs.carrier_of {R : Type u} [CommRing R] (V : FGModuleCat R) :

FGModuleCat.of R ↑V = V

source

theorem vs.addswap_comm {R : Type u} [CommRing R] (M : FGModuleCat R) :

CategoryTheory.CategoryStruct.comp (swap M M).hom (add_hom M) = add_hom M

source

theorem vs.addassoc_comm {R : Type u} [CommRing R] (M : FGModuleCat R) :

CategoryTheory.CategoryStruct.comp (map (add_hom M) (CategoryTheory.CategoryStruct.id M)) (add_hom M) = CategoryTheory.CategoryStruct.comp (assoc M M M).hom (CategoryTheory.CategoryStruct.comp (map (CategoryTheory.CategoryStruct.id M) (add_hom M)) (add_hom M))

source

theorem vs.addinl_comm {R : Type u} [CommRing R] (M : FGModuleCat R) :

CategoryTheory.CategoryStruct.comp (inl M M) (add_hom M) = CategoryTheory.CategoryStruct.id (FGModuleCat.of R ↑M)

source

theorem vs.addinr_comm {R : Type u} [CommRing R] (M : FGModuleCat R) :

CategoryTheory.CategoryStruct.comp (inr M M) (add_hom M) = CategoryTheory.CategoryStruct.id (FGModuleCat.of R ↑M)

source

theorem vs.addsmul_comm {R : Type u} [CommRing R] (M : FGModuleCat R) (a b : R) :

smul_hom M (a + b) = CategoryTheory.CategoryStruct.comp (diag M) (CategoryTheory.CategoryStruct.comp (map (smul_hom M a) (smul_hom M b)) (add_hom (FGModuleCat.of R ↑M)))

source

theorem vs.smuladd_comm {R : Type u} [CommRing R] (M : FGModuleCat R) (a : R) :

CategoryTheory.CategoryStruct.comp (add_hom (FGModuleCat.of R ↑M)) (smul_hom (FGModuleCat.of R ↑M) a) = CategoryTheory.CategoryStruct.comp (map (smul_hom M a) (smul_hom M a)) (add_hom M)

source

@[simp]

theorem vs.swapiso {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] (x : L.obj M × L.obj N) :

L.map (swap M N).hom ((iso L M N).inv x) = (iso L N M).inv (x.2, x.1)

source

@[simp]

theorem vs.map_zero {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] (x : L.obj M) :

L.map 0 x = 0

source

@[simp]

theorem vs.inliso {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] (x : L.obj M) :

L.map (inl M N) x = (iso L M N).inv (x, 0)

source

@[simp]

theorem vs.inriso {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M N : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] (x : L.obj N) :

L.map (inr M N) x = (iso L M N).inv (0, x)

source

@[simp]

theorem vs.associso {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] (x y z : L.obj M) :

L.map (assoc M M M).hom ((iso L (prod M M) M).inv ((iso L M M).inv (x, y), z)) = (iso L M (prod M M)).inv (x, (iso L M M).inv (y, z))

source

@[simp]

theorem vs.diagiso {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] (x : L.obj (FGModuleCat.of R ↑M.obj)) :

L.map (diag M) x = (iso L (FGModuleCat.of R ↑M.obj) (FGModuleCat.of R ↑M.obj)).inv (x, x)

source

noncomputable instance vs.instAddCommMonoidObjFGModuleCat_schlessinger {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] :

AddCommMonoid (L.obj M)

Equations

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

source

instance vs.instModuleObjFGModuleCat_schlessinger {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] :

Module R (L.obj M)

Equations

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

source

noncomputable instance vs.instAddCommGroupObjFGModuleCat_schlessinger {R : Type u} [CommRing R] (L : CategoryTheory.Functor (FGModuleCat R) (Type u)) (M : FGModuleCat R) [CategoryTheory.Limits.PreservesFiniteProducts L] :

AddCommGroup (L.obj M)

Equations

vs.instAddCommGroupObjFGModuleCat_schlessinger L M = Module.addCommMonoidToAddCommGroup R

source

def vs.linmap_of_nattrans {R : Type u} [CommRing R] {L : CategoryTheory.Functor (FGModuleCat R) (Type u)} [CategoryTheory.Limits.PreservesFiniteProducts L] {L' : CategoryTheory.Functor (FGModuleCat R) (Type u)} [CategoryTheory.Limits.PreservesFiniteProducts L'] (η : L ⟶ L') (M : FGModuleCat R) :

L.obj M →ₗ[R] L'.obj M

Equations

vs.linmap_of_nattrans η M = { toFun := η.app M, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

theorem vs.nattrans_eq_linmap {R : Type u} [CommRing R] {L : CategoryTheory.Functor (FGModuleCat R) (Type u)} [CategoryTheory.Limits.PreservesFiniteProducts L] {L' : CategoryTheory.Functor (FGModuleCat R) (Type u)} [CategoryTheory.Limits.PreservesFiniteProducts L'] (η : L ⟶ L') (M : FGModuleCat R) :

η.app M = ⇑(linmap_of_nattrans η M)

source

theorem vs.exists_iso_finmodule {R : Type u} [Field R] (M : FGModuleCat R) :

∃ (n : ℕ), Nonempty (M ≅ FGModuleCat.of R (Fin n → R))

source

instance vs.isIso_natTrans_of_isIso_dim1 {R : Type u} [Field R] {L L' : CategoryTheory.Functor (FGModuleCat R) (Type u)} [CategoryTheory.Limits.PreservesFiniteProducts L] [CategoryTheory.Limits.PreservesFiniteProducts L'] (η : L ⟶ L') [h : CategoryTheory.IsIso (η.app (FGModuleCat.of R R))] :

CategoryTheory.IsIso η