Zulip Chat Archive

Stream: new members

Topic: mono f


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Antoine Labelle (Dec 04 2020 at 03:22):

If so I could just apply it to the direct sum

view this post on Zulip Adam Topaz (Dec 04 2020 at 03:53):

docs#Module.of

view this post on Zulip 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))
#check [add_comm_group V']

everything is fine. What is the problem here?

view this post on Zulip Eric Wieser (Dec 04 2020 at 15:49):

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

view this post on Zulip Eric Wieser (Dec 04 2020 at 15:49):

You want #check (infer_instance : add_comm_group V')

view this post on Zulip 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'"

view this post on Zulip Eric Wieser (Dec 04 2020 at 15:50):

(and [] in that context creates a list)

view this post on Zulip 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