AddCon.hom_ext

Stream: mathlib4

[Kenny Lau]

https://loogle.lean-lang.org/?q=Con%2C+%22ext%22

@Eric Wieser I believe we're currently missing this lemma:

import Mathlib.GroupTheory.Congruence.Hom

namespace Con

variable (M : Type*) {N : Type*} {P : Type*}
variable {M}
variable [MulOneClass M] [MulOneClass N] [MulOneClass P] {c : Con M}

/-- Extensionality for maps `f, g : M⧸~ →* N`: they are equal if their composition with
`mk' : M → M⧸~` are equal. -/
@[to_additive (attr := ext) "Extensionality for maps `f, g : M⧸~ →+ N`: they are equal if their
composition with `mk' : M → M⧸~` are equal."]
lemma hom_ext {f g : c.Quotient →* P} (h : f.comp (mk' c) = g.comp (mk' c)) : f = g :=
  lift_funext _ _ fun x ↦ DFunLike.congr_fun h x

end Con

Should I PR it?

[Eric Wieser]

I agree it should exist

[Eric Wieser]

It should replace funext

[Kenny Lau]

@Eric Wieser I made #26873 . The docstring might need changing. What do you think?

[Eric Wieser]

Sorry, by "replace" I meant "claim the ext attribute from"

[Kenny Lau]

@Eric Wieser resurrected

[Kenny Lau]

@Eric Wieser fixed

[Kenny Lau]

@Eric Wieser added ext