Zulip Chat Archive

Stream: maths

Topic: bundling subgroups -- kernel


view this post on Zulip 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 gker(f)    f(g)=0g\in ker(f)\iff f(g)=0 is definitional, whereas the other definition expands to f(g){0}f(g)\in\{0\} which is defeq to something else

view this post on Zulip Johan Commelin (Mar 07 2020 at 12:16):

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

view this post on Zulip Johan Commelin (Mar 07 2020 at 12:16):

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

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

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

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 12:19):

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

view this post on Zulip Mario Carneiro (Mar 07 2020 at 12:19):

{x | x = 0}

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 12:19):

!

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 12:19):

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

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 12:19):

:D

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

view this post on Zulip Mario Carneiro (Mar 07 2020 at 12:21):

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

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

view this post on Zulip Mario Carneiro (Mar 07 2020 at 12:22):

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

view this post on Zulip Mario Carneiro (Mar 07 2020 at 12:22):

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

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

view this post on Zulip Mario Carneiro (Mar 07 2020 at 12:24):

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

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

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 12:26):

and mem_singleton would be rfl

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

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

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

view this post on Zulip Mario Carneiro (Mar 07 2020 at 12:41):

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

view this post on Zulip Mario Carneiro (Mar 07 2020 at 12:41):

and mem has type A -> B -> Prop

view this post on Zulip Mario Carneiro (Mar 07 2020 at 12:41):

so nothing there says what B is

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 12:42):

nice catch -- thanks.

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

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

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 13:26):

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

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 13:31):

Aah, simp does it.

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

view this post on Zulip Mario Carneiro (Mar 10 2020 at 04:02):

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

view this post on Zulip Mario Carneiro (Mar 10 2020 at 04:03):

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

view this post on Zulip Mario Carneiro (Mar 10 2020 at 04:03):

so it would require changes to the C++

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

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

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