bundling subgroups -- kernel

Stream: maths

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

{x | x = 0}

[Kevin Buzzard]

!

[Kevin Buzzard]

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

[Kevin Buzzard]

:D

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

and mem_singleton would be rfl

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

and mem has type A -> B -> Prop

[Mario Carneiro]

so nothing there says what B is

[Kevin Buzzard]

nice catch -- thanks.

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

Aah, simp does it.

[Yury G. Kudryashov]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

so it would require changes to the C++

[Mario Carneiro]

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]

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]

(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.)