## Stream: new members

### Topic: mono f

#### Antoine Labelle (Dec 03 2020 at 21:01):

import tactic
import algebra.algebra.basic
import linear_algebra.direct_sum_module
import category_theory.simple
import algebra.category.Module.abelian

open category_theory
open_locale direct_sum

universes v u

variables {k : Type} [field k] {A : Type} [ring A] [algebra k A]
variables {I : Type} {finI  : fintype I}
variables {V : I → Module.{v} A} [∀i:I, simple (V i)] {m : I → ℕ}
variables {W : Module.{v} A} {f : W → (⨁ i, (⨁ i': fin (m i), V i))} [mono f]


Does someone see why [mono f] yields an error?

#### Reid Barton (Dec 03 2020 at 21:19):

f would need to use the "long arrow" \hom, but then I don't know what the right way to write the direct sums is.

#### Antoine Labelle (Dec 04 2020 at 03:21):

Hum, is there a way to convert modules as types with instance of [module A M] to modules as elements of the category of modules?

#### Antoine Labelle (Dec 04 2020 at 03:22):

If so I could just apply it to the direct sum

docs#Module.of

#### Antoine Labelle (Dec 04 2020 at 15:43):

So def V' := Module.of A (⨁ i, (⨁ i': fin (m i), V i)) give the error

failed to synthesize type class instance for
A : Type u,
_inst_2 : ring A,
I : Type,
V : I → Module A,
_inst_4 : Π (i : I), simple (V i),
m : I → ℕ
⊢ add_comm_group (⨁ (i : I) (i' : fin (m i)), ↥(V i))


However if I do

def V' := (⨁ i, (⨁ i': fin (m i), V i))


everything is fine. What is the problem here?

#### Eric Wieser (Dec 04 2020 at 15:49):

#check [add_comm_group V'] is showing you information about a term of type list Type

#### Eric Wieser (Dec 04 2020 at 15:49):

You want #check (infer_instance : add_comm_group V')

#### Eric Wieser (Dec 04 2020 at 15:50):

Ie "show me a thing that is a term of type add_comm_group V'" instead of just "show me the type add_comm_group V'"

#### Eric Wieser (Dec 04 2020 at 15:50):

(and [] in that context creates a list)

#### Antoine Labelle (Dec 04 2020 at 15:53):

#check (infer_instance : add_comm_group V') doesn't yield errors but this doesn't solve my problem for converting to Module A

Last updated: May 10 2021 at 23:11 UTC