polynomial.ring_hom_ext

Stream: maths

[Chris Hughes]

The statement of polynomial.ring_hom_ext is currently

lemma ring_hom_ext {S} [semiring S] {f g : polynomial R →+* S}
  (h₁ : ∀ a, f (C a) = g (C a)) (h₂ : f X = g X) : f = g :=

Should the assumption ∀ a, f (C a) = g (C a) be changed to f.comp C = g.comp C? That way it's easier to apply another hom ext lemma to prove that equality if there is a hom ext lemma about maps out of R.

[Kevin Buzzard]

Nice observation!

[Shing Tak Lam]

https://leanprover-community.github.io/mathlib_docs/notes.html#partially-applied%20ext%20lemmas right?

[Eric Wieser]

I think I meant to PR this and forgot

[Eric Wieser]

docs#add_monoid_algebra.ring_hom_ext' gets it right.

[Eric Wieser]

So I guess we should have docs#polynomial.ring_hom_ext'

[Eric Wieser]

... which we do

[Eric Wieser]

So no action needed here?

[Eric Wieser]

Other than adding a /-- See note [partially-applied ext lemmas] -/ docstring to it, maybe

[Chris Hughes]

I think maybe making ext' the primary version would be good.

[Yury G. Kudryashov]

I usually tried to make lemma *.*_ext with something like ∀ a, f (C a) = g (C a) and @[ext] *.*_ext' version with f.comp C = g.comp C.

[Yury G. Kudryashov]

I wonder whether ext should automatically call dsimp (may be, with custom settings) to get rid of all those auxiliary homs.

[Eric Wieser]

Also, #9235 is about mv_polynomial not polynomial; I think the former is missing this generalization

[Chris Hughes]

I think the approach in #9235 is still wrong, it's best to take the same approach as with polynomial and just make a new lemma.

[Eric Wieser]

Sure, but you'll still want most of the downstream changes in that PR

[Eric Wieser]

So it's probably worth continuing from rather than starting over

[Chris Hughes]

I don't actually think I do want most of the downstream changes. Mostly I was fixing things with apply rather than ext

[Chris Hughes]

I reopened it.

[Chris Hughes]

the data/mv_polynomial and ring_theory/mv_polynomial folders build locally, so I'll wait for ci to check the rest

[Chris Hughes]

We still don't use follow the convention in the note when it comes to maps of Types. We still have the assumption ∀ (i : σ), ⇑f (X i) = ⇑g (X i). I just had an example where σ was option _ and if we'd had the assumption f ∘ X = g ∘ X then I could have applied an extensionality lemma for maps out of option _. Not sure if we want to go this far though.

[Eric Wieser]

Does ext (_ | x) work for option?

[Eric Wieser]

My mental model is that ext is like a version of cases that discharges most of the hypotheses using properties of morphisms

[Yury G. Kudryashov]

I think, we should have custom ext lemmas for maps from quotients.

[Yury G. Kudryashov]

OTOH, we can just use ext ⟨x⟩.

[Eric Wieser]

The custom lemmas can preserve morphism properties though