quotient modules exists_rep

Stream: new members

[Daan van Gent]

I am trying to prove some facts about quotient modules, and I got stuck on something that boils down to the following.
Even though lean agrees that coker is well defined, in the example it seems to forget that im R f induces a valid equivalence relation.
What am I doing wrong?
As a side question: it feels like the things I am trying to do should be in lean somewhere, but I cannot seem to find them.

import algebra.module.submodule.basic
import ring_theory.simple_module

variables (R : Type*) {M N : Type*} [ring R] [add_comm_group M] [module R M] [add_comm_group N]
  [module R N] (f : M →ₗ[R] N)

def im : submodule R N := {
  carrier := f '' ⊤,
  add_mem' := sorry,
  zero_mem' := sorry,
  smul_mem' := sorry
}

def coker := N ⧸ im R f

example (x : coker R f) : ∃ y : N, submodule.quotient.mk y = x :=
begin
  exact quotient.exists_rep x,
end

[Eric Rodriguez]

@@quotient.exists_rep (im R f).quotient_rel x works but I'm not sure why this isn't working as is...

[Eric Rodriguez]

also, is this docs#submodule.map of top?

[Daan van Gent]

Thanks! I can work with that. I am still curious why the above code does not work, because I might be doing something wrong.

It is indeed submodule.map, which is helpful. It seems like a lot of the things I need are actually in linear_map instead modules. The naming scheme is still a bit confusing to me.

[Eric Wieser]

I think you're looking for docs#linear_map.range?

[Daan van Gent]

Eric Wieser said:

I think you're looking for docs#linear_map.range?

I guess, but I am mainly interested in why quotient.exists_rep fails. I run in to similar problems with groups and quotients it seems, in the following very artificial example:

import group_theory.quotient_group

open group
open subgroup
open quotient_group

example (G : Type*) [group G] (I J: subgroup G) (hIJ : I = J)
  (h : ∃ [hN : normal $ subgroup_of I J], @is_simple_group _ $ @quotient.group _ _ _ hN)
  : false :=
begin
  cases h with hN hs,
  cases hs with hp,
  rcases hp with ⟨x, y, hxy⟩,
  apply hxy,
  --have hg : group (↥J ⧸ subgroup_of I J) := @quotient.group _ _ _ hN, -- pointless
  have hx : x = 1,
  -- failed to synthesize type class instance for has_one
end

The typeclass system feels very fragile, but I must be using it wrong.

[Eric Wieser]

This is a better way to spell what you have there:

import group_theory.quotient_group

open group
open subgroup
open quotient_group

example (G : Type*) [group G] (I J: subgroup G) (hIJ : I = J)
  (h : ∃ [hN : normal $ subgroup_of I J], by exactI is_simple_group (↥J ⧸ I.subgroup_of J))
  : false :=
begin
  casesI h with hN hs,
  obtain ⟨x, y, hxy⟩ := exists_pair_ne (↥J ⧸ subgroup_of I J),
  apply hxy,
  have hx : x = 1,
  sorry
end

[Eric Wieser]

In general:

• If you have a typeclass in an existential, use casesI not cases, to ensure it enters the context
• Don't call cases on typeclass arguments, look for the API lemma you're supposed to use instead (in this case, exists_pair_ne)

[Alex J. Best]

For efficiency reasons the typeclass cache isn't automatically reset all the time during tactic proofs.
This means that if you introduce a typeclass hypothesis (like subgroup.normal) during a proof you need to instruct lean to reset the cache.
Many tactics have I version that does this for you.