## Stream: maths

### Topic: Extensionality of homs

#### 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?

#### 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.

#### 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)

#### 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


#### 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.

#### Kevin Buzzard (Jul 18 2020 at 10:51):

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

#### 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.

#### Yury G. Kudryashov (Jul 18 2020 at 20:19):

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

#### 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.

#### Yury G. Kudryashov (Jul 18 2020 at 20:21):

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

#### 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?

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

#### 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"?

#### Chris Hughes (Jul 18 2020 at 21:57):

I meant equality of elements.

#### Chris Hughes (Jul 18 2020 at 21:57):

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