[Merged by Bors] - feat(data/sym2): add the universal property, and make sym2.is_diag ⟦(x, y)⟧ ↔ x = y true definitionally
#8358
Conversation
eric-wieser
commented
Jul 18, 2021
eric-wieser
commented
…(x, y)⟧ ↔ x = y` true definitionally
eric-wieser
force-pushed
the
eric-wieser/sym2.lift
branch
from
2000e6b
to
2afd995
Compare
eric-wieser
added
the
awaiting-review
| prod.rec_on z $ λ _ _, is_diag_iff_eq | ||
|
|
||
| @[simp] | ||
| lemma diag_is_diag (a : α) : is_diag (diag a) := |
There was a problem hiding this comment.
| lemma diag_is_diag (a : α) : is_diag (diag a) := | |
| lemma is_diag_diag (a : α) : is_diag (diag a) := |
And the appropriate edits below
There was a problem hiding this comment.
This name is the same as it was before this PR, but I suppose I could creep the scope to fix the name.
There was a problem hiding this comment.
I get confused about the name to give compositions like this, and I get even more confused when dot notation is involved. If the conclusion were written as (diag a).is_diag (which it could be), would it still be is_diag_diag?
I think I'm guilty putting is_foo predicates at the ends of lemmas elsewhere, too, which is why I ask.
There was a problem hiding this comment.
I made a Zulip thread.
There was a problem hiding this comment.
I've also reverted the change - if it's contentious, then renaming it is outside the scope of this PR.
src/data/sym2.lean
Outdated
| `sym2.from_rel` is a more convenient spelling when working with `Prop`. -/ | ||
| def lift {β : Sort*} : | ||
| {f : α → α → β // ∀ a₁ a₂, f a₁ a₂ = f a₂ a₁} ≃ (sym2 α → β) := | ||
| { to_fun := λ f, quotient.lift (λ a : α × α, (f : α → α → β) a.1 a.2) $ |
There was a problem hiding this comment.
Could you please make that to_fun a separate definition? We needed that generalisation of sym2.from_rel some time ago.
There was a problem hiding this comment.
What would be the point of the separate definition? If you use lift it unfolds to this anyway.
There was a problem hiding this comment.
Well I guess it's easier to have a definition without mentioning a subtype.
def from_fun {β : Sort*} {f : α → α → β} (comm : ∀ ⦃x y⦄, f x y = f y x) :
sym2 α → β :=
quotient.lift (uncurry f) (by { rintro ⟨x, y⟩ _ ⟨_, _⟩, {refl }, unfold uncurry, rw comm })
There was a problem hiding this comment.
That def results in {β : Type*} since uncurry isn't defined on sorts:
#check @from_fun
-- Π {α : Type u_1} {β : Type u_2} {f : α → α → β}, (∀ ⦃x y : α⦄, f x y = f y x) → sym2 α → βThere was a problem hiding this comment.
Oh that's annoying... There's no real reason for it, right?
There was a problem hiding this comment.
Wait, what? The original definition of from_rel uses function.uncurry r. What is this witchcraft?
There was a problem hiding this comment.
Looking again, it looks like there's no point in letting lift work on Sort anyway, no one every needs a subtype of a proof, and quotient.induction works just fine for the cases when Sort would apply.
src/data/sym2.lean
Outdated
| `sym2.from_rel` instead. -/ | ||
| def lift {β : Type*} : {f : α → α → β // ∀ a₁ a₂, f a₁ a₂ = f a₂ a₁} ≃ (sym2 α → β) := | ||
| { to_fun := λ f, quotient.lift (uncurry ↑f) $ by { rintro _ _ ⟨⟩, exacts [rfl, f.prop _ _] }, | ||
| inv_fun := λ F, ⟨λ a₁ a₂, F ⟦(a₁, a₂)⟧, λ a₁ a₂, congr_arg F eq_swap⟩, |
There was a problem hiding this comment.
If we want to maintain the point-free style of to_fun, then inv_fun could be
inv_fun := λ F, ⟨curry (F ∘ quotient.mk), λ a₁ a₂, congr_arg F eq_swap⟩,There was a problem hiding this comment.
Sure, why not. I added a lemma that unfolds it to my version, but it's nice to see the composition in lift.inv_fun, since there almost always is one.
Since there's no consensus, lets leave renaming this for another time. Also adds a docstring and a lemma
eric-wieser
force-pushed
the
eric-wieser/sym2.lift
branch
from
1a2ff4b
to
4dd20f2
Compare
There was a problem hiding this comment.
Looks good to me! I don't have a strong opinion on the is_diag_diag naming choice, so I'll let @eric-wieser decide what to do there.
bors d+
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors r+ I've left the name untouched, someone else can do a wider rename in a separate PR. |
…(x, y)⟧ ↔ x = y` true definitionally (#8358)
github-actions
bot
added
the
ready-to-merge
|
Build failed: |
|
bors r+ |
…(x, y)⟧ ↔ x = y` true definitionally (#8358)
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
sym2.is_diag ⟦(x, y)⟧ ↔ x = y true definitionallysym2.is_diag ⟦(x, y)⟧ ↔ x = y true definitionally
