## Stream: maths

### Topic: bundling subgroups -- kernel

#### Kevin Buzzard (Mar 07 2020 at 12:12):

What's the best definition of kernel? Are there arguments in both directions?

def ker (f : G →+ H) : add_subgroup G := (⊥ : add_subgroup H).comap f

def ker' (f : G →+ H) : add_subgroup G :=
{ carrier := {g : G | f g = 0},
zero_mem := ...
...
}


The difference is that with the second definition $g\in ker(f)\iff f(g)=0$ is definitional, whereas the other definition expands to $f(g)\in\{0\}$ which is defeq to something else

#### Johan Commelin (Mar 07 2020 at 12:16):

My gut feeling would say, go for (2).

#### Johan Commelin (Mar 07 2020 at 12:16):

But you'll want a lemma that says that the two definition are equal anyway.

#### Kevin Buzzard (Mar 07 2020 at 12:17):

Sure, this is purely a question of which one you want to be the definition and which one you want to be the theorem. But I don't have any real criteria for deciding.

#### Mario Carneiro (Mar 07 2020 at 12:18):

Alternatively you could step back to \bot itself, to fix the definition so that you get the definitional equality you want with the first version

#### Kevin Buzzard (Mar 07 2020 at 12:19):

\bot is a subgroup of H so I need to define the carrier set.

#### Mario Carneiro (Mar 07 2020 at 12:19):

{x | x = 0}

!

#### Kevin Buzzard (Mar 07 2020 at 12:19):

If I do it like this then they're probably defeq.

:D

#### Mario Carneiro (Mar 07 2020 at 12:20):

I feel like a lot of things would be simpler if this was the definition of singleton 0

#### Mario Carneiro (Mar 07 2020 at 12:21):

maybe we should remove the definition of singleton from init.core?

#### Kevin Buzzard (Mar 07 2020 at 12:21):

One could imagine that notation could handle this somehow -- {} expands to false and {x} to what you just said and then {a,b} could mean {x | x = a \or x = b} etc.

#### Mario Carneiro (Mar 07 2020 at 12:22):

the idea that singleton a = insert a empty in all circumstances is probably a bad idea

#### Mario Carneiro (Mar 07 2020 at 12:22):

but the definition is in core, in the very first file

#### Mario Carneiro (Mar 07 2020 at 12:23):

we have a typeclass has_insert, so we could have has_singleton as well for the version in core to bind to

#### Mario Carneiro (Mar 07 2020 at 12:24):

and then the {a, ..., z} notation expands to insert a (insert b ... (singleton z))

#### Kevin Buzzard (Mar 07 2020 at 12:26):

This would probably break a lot of stuff in a good way i.e. the fix would be "make it a bit simpler"

#### Kevin Buzzard (Mar 07 2020 at 12:26):

and mem_singleton would be rfl

#### Mario Carneiro (Mar 07 2020 at 12:28):

it is very often that I am too lazy or golfy to go find the relevant theorem and given a \in {b} use rcases h with rfl|<<>> to get at the value. This idiom would get simpler

#### Kevin Buzzard (Mar 07 2020 at 12:38):

set_option pp.notation false

example (α : Type) (s t : α) : t ∈ {s} :=
begin
unfold singleton,
-- there's a metavariable in the goal?!
/-
⊢ has_mem.mem t (has_insert.insert s (has_emptyc.emptyc ?m_1))
-/
sorry
end

/-
tactic failed, result contains meta-variables
state:
no goals
-/


I was trying to work out what t ∈ {s} was defeq to and I think I broke something

#### Mario Carneiro (Mar 07 2020 at 12:40):

Notice that both {s} : set α and {s} : finset α would be consistent with your theorem statement. I imagine that if you use theorem T instead of example you will get an error

#### Mario Carneiro (Mar 07 2020 at 12:41):

it's because insert has type A -> B -> B

#### Mario Carneiro (Mar 07 2020 at 12:41):

and mem has type A -> B -> Prop

#### Mario Carneiro (Mar 07 2020 at 12:41):

so nothing there says what B is

#### Kevin Buzzard (Mar 07 2020 at 12:42):

nice catch -- thanks.

#### Kevin Buzzard (Mar 07 2020 at 12:59):

Just to confirm that {s} currently expands to {b : α | b = s ∨ false} -- I was going to say this in the first post but then I got distracted by the example/theorem thing

#### Kevin Buzzard (Mar 07 2020 at 13:23):

I can't solve the analogous question for range though. If I use set.univ for top (which is {x | true}) and define range to be map top then mem_range (h is in the range iff there exists g with f(g) = h) isn't rfl, it's

example (α : Type) (P : α → Prop) :
(∃ a, true ∧ P a) ↔ (∃ a, P a)


library_search couldn't find this in logic.basic.

#### Kevin Buzzard (Mar 07 2020 at 13:26):

Indeed, for set.range they just define it directly so mem_range is rfl.

#### Kevin Buzzard (Mar 07 2020 at 13:31):

Aah, simp does it.

#### Yury G. Kudryashov (Mar 10 2020 at 03:03):

Last time I checked {a, b} expanded to insert b {a}, not insert a {b}. I think, it would be nice to change this but my knowledge of lean notation syntax is not good enough.

#### Mario Carneiro (Mar 10 2020 at 04:02):

This is an easy change to core, although it will cause lots of breakage

#### Mario Carneiro (Mar 10 2020 at 04:03):

Oh! The notation for {a, ..., z} is actually never declared, it is lean magic

#### Mario Carneiro (Mar 10 2020 at 04:03):

so it would require changes to the C++

#### Mario Carneiro (Mar 10 2020 at 04:05):

in a way that's a good thing since I'm not sure it's possible to define {} = empty and {a, b, c} = insert a (insert b (singleton c)) as proposed in another thread using the lean 3 notation syntax, which is quite limited

#### Mario Carneiro (Mar 10 2020 at 04:13):

Actually, it looks like lean already does the case distinction between empty and nonempty cases. Look what happens if I make my own prelude:

prelude

def has_emptyc.emptyc (α : Type) : α := sorry
def singleton {α} (a : α) : α := sorry
def has_insert.insert {α} (a b : α) : α := sorry

variables (a b c : Type)
#check {}  -- has_emptyc.emptyc ?M_1 : ?M_1
#check {a} -- singleton a : Type
#check {a} -- singleton a : Type
#check {a, b} -- has_insert.insert b (singleton a) : singleton a
#check {a, b, c} -- has_insert.insert c (has_insert.insert b (singleton a)) : Type


The built in notation parser doesn't actually know what the functions has_insert.insert and singleton are, it just writes these expressions down and hands them off to the elaborator. So really all that is necessary is to remove the definition of singleton and replace it with a typeclass to enable the {0} = {x | x = 0} defeq. However as you can see the order is still flipped; the C++ has to be changed to fix this

#### Mario Carneiro (Mar 10 2020 at 04:15):

(If you are wondering why {a, ..., z} is baked into lean like this, while [a, ... z] is not, it's because lean has to disambiguate the various notations that start with {, e.g. {x // p x}, {x | p x} and {x, y}, and this requires more lookahead than the normal notation parser can tolerate.)

Last updated: May 06 2021 at 18:20 UTC