Zulip Chat Archive

Stream: maths

Topic: Extensionality of homs


view this post on Zulip Chris Hughes (Jul 18 2020 at 10:21):

Currently the ext attribute for monoid_hom is assigned to the lemma that says maps are equal if they're equal after being applied everywhere, funext basically. This isn't the extensionality we always want to use though. Colimitty types have extensionality lemmas for homs out of the type. e.g. maps out of the free group are equal iff they're equal on the basis, maps out of the polynomial ring are equal iff they're equal on the base ring and X. These are usually more useful than proving the equality by funext. Can/should we set higher priority to these extensionality lemmas?

view this post on Zulip Chris Hughes (Jul 18 2020 at 10:22):

Incidentally, I think these lemmas are quite powerful and a lot of the commutativity headaches will become easy with lots of these extensionality lemmas.

view this post on Zulip Chris Hughes (Jul 18 2020 at 10:24):

This is a headache for polynomial ring I remember that becomes quite simple with the extensionality of homs. p.eval₂ (g ∘ f) (f x) = g (p.eval₂ f x)

view this post on Zulip Kevin Buzzard (Jul 18 2020 at 10:42):

I don't know about should (although my guess is yes), but as for "can" I think we can. This came up when I was experimenting with my LftCM subgroup talk:

import tactic

universe u

@[ext] structure submonoid (G : Type u) [monoid G] :=
(carrier : set G)
(mul_mem' :  {a b : G}, a  carrier  b  carrier  a * b  carrier)
(one_mem' : (1 : G)  carrier)

namespace submonoid

#check ext -- ∀ (x y : submonoid ?M_1), x.carrier = y.carrier → x = y

variables {G : Type u} [monoid G]

instance : has_mem G (submonoid G) := ⟨λ g H, g  H.carrier

variables {H J : submonoid G}

@[ext] lemma ext' (h :  x : G, x  H  x  J) : H = J :=
begin
  ext x,
  -- ⊢ x ∈ H.carrier ↔ x ∈ J.carrier
  exact h x,
end

-- I have no idea what the default priorities are

#print ext -- @[_ext_lemma_core] blah
#print ext' -- @[_ext_lemma_core, ext list.nil.{0} ext_param_type] blah


-- check that ext' beats ext
lemma test (H J : submonoid G) : H = J :=
begin
  ext x, -- ⊢ x ∈ H ↔ x ∈ J
  sorry
end

attribute [ext, priority 10] ext'
attribute [ext, priority 10000] ext

-- check that ext beats ext' now
lemma test2 (H J : submonoid G) : H = J :=
begin
  ext x, -- x ∈ H.carrier ↔ x ∈ J.carrier
  sorry
end

#print ext -- @[_ext_lemma_core, priority 10000, ext list.nil.{0} ext_param_type, priority 10000] blah
#print ext' -- @[_ext_lemma_core, priority 10, ext list.nil.{0} ext_param_type, priority 10] blah

end submonoid

view this post on Zulip Kevin Buzzard (Jul 18 2020 at 10:46):

Randomly reprioritising attributes might break code so should presumably only be done at the point of definition.

view this post on Zulip Kevin Buzzard (Jul 18 2020 at 10:51):

Wait -- it's more subtle than I'd realised. I'll start a separate thread.

view this post on Zulip Scott Morrison (Jul 18 2020 at 10:54):

I think this would be a great idea. ext works great for this throughout the limits library.

view this post on Zulip Yury G. Kudryashov (Jul 18 2020 at 20:19):

We have a few "specialized" ext lemmas, and I think that we should have more.

view this post on Zulip Yury G. Kudryashov (Jul 18 2020 at 20:21):

Note that, e.g., for quotient it's better to say f.comp mk = g.comp mk (don't remember the name of mk : G → quotient H), not ∀ x ∈ G, f (mk x) = g (mk x). Then for G = free_group α, ext will use free_group.hom_ext after this ext.

view this post on Zulip Yury G. Kudryashov (Jul 18 2020 at 20:21):

(again, I don't remember what is the current name of free_group.hom_ext).

view this post on Zulip Chris Hughes (Jul 18 2020 at 21:10):

This does break what I thought was the obvious wisdom that you always prove functions are equal by proving they're equal on all elements. Does it make sense to adopt the convention that we don't state commutativity assumption as an equality of assumptions from now on?

view this post on Zulip Yury G. Kudryashov (Jul 18 2020 at 21:21):

If G has no specialized ext lemma, then ext will apply monoid_hom.ext next resulting in ∀ x ∈ G, f (mk x) = g (mk x).

view this post on Zulip Yury G. Kudryashov (Jul 18 2020 at 21:21):

What do you mean by "we don't state commutativity assumption as an equality of assumptions"?

view this post on Zulip Chris Hughes (Jul 18 2020 at 21:57):

I meant equality of elements.

view this post on Zulip Chris Hughes (Jul 18 2020 at 21:57):

Bad typo.

view this post on Zulip Chris Hughes (Jul 18 2020 at 21:58):

So we should have (f.comp g = h.comp i) as assumption to lemmas instead of ∀ x, f (g x) = h (i x)


Last updated: May 10 2021 at 08:14 UTC