kernels of homomorphisms

Stream: general

[Johan Commelin]

Ok, I'm making my feet wet with a first attempt at formalising something. I want to say write down the assumption im(f) = ker(g), where f and g are group homomorphisms. I guess im(f) will be something like f ' A.univ. I tried to find kernels in algebra.group but did not find anything. Are kernels somewhere else?

[Andrew Ashworth]

https://github.com/leanprover/mathlib/search?utf8=✓&q=ker&type=

[Andrew Ashworth]

it's a little sparse

[Johan Commelin]

Aah, ok. So I should use the github search for this. Thanks

[Johan Commelin]

What am I doing wrong here?

universes u
variables
{A : Type u} [group A]
{B : Type u} [group B]
{f : A → B} [is_group_hom f]

definition ker f := is_group_hom.ker f
definition im f := f '' (@univ A)

[Johan Commelin]

Lean does not like my definition of ker andim

[Johan Commelin]

I get squiggles under the f

[Johan Commelin]

invalid binder declaration, delimiter/bracket expected (i.e., '(', '{', '[', '{{')

[Reid Barton]

You can write

variables (f)
definition ker := is_group_hom.ker f
definition im := f '' (@univ A)

though I'm not sure whether it is very good style

[Patrick Massot]

Could use def im := set.range f

[Kevin Buzzard]

definition ker f := ... is no good because everything to the left of the := has to either be a variable and skipped completely, or a term together with its type. Just f by itself doesn't work.

[Kevin Buzzard]

As Reid Barton says, you can skip the f completely

[Kevin Buzzard]

but you might want to write

import group_theory.subgroup
universes u
variables {A : Type u} [group A] {B : Type u} [group B]

definition ker (f : A → B) [is_group_hom f] := is_group_hom.ker f

[Patrick Massot]

Why do you want to enforce the same universe?

[Kevin Buzzard]

Patrick, although your comment is of course sensible, and probably Johan should write universes u v and then {B : Type v}, in ZFC we only have universe and it never bothered us before :-)

[Patrick Massot]

If you don't care (like I don't care) then use Type* until it bites you

[Mario Carneiro]

The lean syntax requires parentheses around arguments left of :=, so def ker (f) := ... would work. But it would be a different f than the one in the variable statement, so its type could be different (it will be inferred) and in particular it will not be assumed to be a group_hom

[Mario Carneiro]

By the way, the parentheses used to be optional, until we discovered that it enables the following evil example:

example inconsistent : false := trivial

(hint: it's not proving false)