# Zulip Chat Archive

## Stream: new members

### Topic: quotient modules exists_rep

#### Daan van Gent (Oct 17 2022 at 09:35):

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 (Oct 17 2022 at 10:10):

`@@quotient.exists_rep (im R f).quotient_rel x`

works but I'm not sure why this isn't working as is...

#### Eric Rodriguez (Oct 17 2022 at 10:13):

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

#### Daan van Gent (Oct 17 2022 at 10:26):

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 (Oct 17 2022 at 12:45):

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

#### Daan van Gent (Oct 17 2022 at 13:21):

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 (Oct 17 2022 at 13:49):

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 (Oct 17 2022 at 13:49):

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 (Oct 17 2022 at 13:49):

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.

Last updated: Dec 20 2023 at 11:08 UTC