Extensionality of homs

Stream: maths

[Chris Hughes]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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]

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

[Chris Hughes]

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]

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]

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

[Chris Hughes]

I meant equality of elements.

[Chris Hughes]

Bad typo.

[Chris Hughes]

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