mono f

Stream: new members

[Antoine Labelle]

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]

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]

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]

If so I could just apply it to the direct sum

[Adam Topaz]

docs#Module.of

[Antoine Labelle]

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))
#check [add_comm_group V']

everything is fine. What is the problem here?

[Eric Wieser]

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

[Eric Wieser]

You want #check (infer_instance : add_comm_group V')

[Eric Wieser]

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]

(and [] in that context creates a list)

[Antoine Labelle]

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