From 0cf652575ff6bea024bb3cf89c56e6ca4034e72f Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 2 Jun 2019 19:06:37 -0400 Subject: [PATCH 1/3] feat(data/equiv/basic): improve arrow_congr, define conj - redefine `equiv.arrow_congr` without an enclosing `match` - prove some trivial lemmas about `equiv.arrow_congr` - define `equiv.conj`, and prove trivial lemmas about it --- src/data/equiv/basic.lean | 50 ++++++++++++++++++++++++++++++++++----- 1 file changed, 44 insertions(+), 6 deletions(-) diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean index 6f28f04e9ec91..a3ca1bca16da8 100644 --- a/src/data/equiv/basic.lean +++ b/src/data/equiv/basic.lean @@ -212,12 +212,50 @@ protected def ulift {α : Type u} : ulift α ≃ α := protected def plift : plift α ≃ α := ⟨plift.down, plift.up, plift.up_down, plift.down_up⟩ -@[congr] def arrow_congr {α₁ β₁ α₂ β₂ : Sort*} : α₁ ≃ α₂ → β₁ ≃ β₂ → (α₁ → β₁) ≃ (α₂ → β₂) -| ⟨f₁, g₁, l₁, r₁⟩ ⟨f₂, g₂, l₂, r₂⟩ := - ⟨λ (h : α₁ → β₁) (a : α₂), f₂ (h (g₁ a)), - λ (h : α₂ → β₂) (a : α₁), g₂ (h (f₁ a)), - λ h, by funext a; dsimp; rw [l₁, l₂], - λ h, by funext a; dsimp; rw [r₁, r₂]⟩ +@[congr] def arrow_congr {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : (α₁ → β₁) ≃ (α₂ → β₂) := +{ to_fun := λ f, e₂.to_fun ∘ f ∘ e₁.inv_fun, + inv_fun := λ f, e₂.inv_fun ∘ f ∘ e₁.to_fun, + left_inv := λ f, funext $ λ x, by dsimp; rw [e₂.left_inv, e₁.left_inv], + right_inv := λ f, funext $ λ x, by dsimp; rw [e₂.right_inv, e₁.right_inv] } + +lemma arrow_congr_apply {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (f : α₁ → β₁) : + arrow_congr e₁ e₂ f = e₂.to_fun ∘ f ∘ e₁.inv_fun := +rfl + +lemma arrow_congr_comp_apply {α₁ β₁ γ₁ α₂ β₂ γ₂ : Sort*} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (eg : γ₁ ≃ γ₂) + (f : α₁ → β₁) (g : β₁ → γ₁) (x : α₂) : + arrow_congr ea eg (g ∘ f) x = arrow_congr eb eg g (arrow_congr ea eb f x) := +show (eg $ g $ f $ ea.inv_fun x) = (eg $ g $ eb.inv_fun $ eb $ f $ ea.inv_fun x), +by unfold_coes; rw eb.left_inv + +lemma arrow_congr_refl {α β : Sort*} : + arrow_congr (equiv.refl α) (equiv.refl β) = equiv.refl (α → β) := rfl + +lemma arrow_congr_trans {α₁ β₁ α₂ β₂ α₃ β₃ : Sort*} + (e₁ : α₁ ≃ α₂) (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃) : + (arrow_congr e₁ e₁').trans (arrow_congr e₂ e₂') = arrow_congr (e₁.trans e₂) (e₁'.trans e₂') := +rfl + +lemma arrow_congr_symm {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : + (arrow_congr e₁ e₂).symm = arrow_congr e₁.symm e₂.symm := +rfl + +def conj (e : α ≃ β) : (α → α) ≃ (β → β) := arrow_congr e e + +lemma conj_refl : conj (equiv.refl α) = equiv.refl (α → α) := rfl + +lemma conj_symm (e : α ≃ β) : e.symm.conj = e.conj.symm := rfl + +lemma conj_trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : + (e₁.trans e₂).conj = e₁.conj.trans e₂.conj := +rfl + +lemma conj_apply (e : α ≃ β) (f : α → α) : e.conj f = e.to_fun ∘ f ∘ e.inv_fun := +rfl + +lemma conj_comp_apply (e : α ≃ β) (f₁ f₂ : α → α) (y : β) : + e.conj (f₁ ∘ f₂) y = e.conj f₁ (e.conj f₂ y) := +by apply arrow_congr_comp_apply def punit_equiv_punit : punit.{v} ≃ punit.{w} := ⟨λ _, punit.star, λ _, punit.star, λ u, by cases u; refl, λ u, by cases u; reflexivity⟩ From f50132bc04db943c0cdfeae52d8c463a0dce2b57 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Fri, 7 Jun 2019 11:16:44 -0400 Subject: [PATCH 2/3] chore(data/equiv/basic): add @[simp] Also split some long lines, and swap lhs with rhs in a few lemmas. --- src/data/equiv/basic.lean | 37 ++++++++++++++++++++----------------- 1 file changed, 20 insertions(+), 17 deletions(-) diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean index a3ca1bca16da8..51dd1420b6ee1 100644 --- a/src/data/equiv/basic.lean +++ b/src/data/equiv/basic.lean @@ -212,48 +212,51 @@ protected def ulift {α : Type u} : ulift α ≃ α := protected def plift : plift α ≃ α := ⟨plift.down, plift.up, plift.up_down, plift.down_up⟩ -@[congr] def arrow_congr {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : (α₁ → β₁) ≃ (α₂ → β₂) := +@[congr] def arrow_congr {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : + (α₁ → β₁) ≃ (α₂ → β₂) := { to_fun := λ f, e₂.to_fun ∘ f ∘ e₁.inv_fun, inv_fun := λ f, e₂.inv_fun ∘ f ∘ e₁.to_fun, left_inv := λ f, funext $ λ x, by dsimp; rw [e₂.left_inv, e₁.left_inv], right_inv := λ f, funext $ λ x, by dsimp; rw [e₂.right_inv, e₁.right_inv] } -lemma arrow_congr_apply {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (f : α₁ → β₁) : - arrow_congr e₁ e₂ f = e₂.to_fun ∘ f ∘ e₁.inv_fun := +@[simp] lemma arrow_congr_apply {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) + (f : α₁ → β₁) (x : α₂) : + arrow_congr e₁ e₂ f x = (e₂ $ f $ e₁.symm x) := rfl -lemma arrow_congr_comp_apply {α₁ β₁ γ₁ α₂ β₂ γ₂ : Sort*} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (eg : γ₁ ≃ γ₂) - (f : α₁ → β₁) (g : β₁ → γ₁) (x : α₂) : - arrow_congr ea eg (g ∘ f) x = arrow_congr eb eg g (arrow_congr ea eb f x) := -show (eg $ g $ f $ ea.inv_fun x) = (eg $ g $ eb.inv_fun $ eb $ f $ ea.inv_fun x), -by unfold_coes; rw eb.left_inv +/- TODO: why Lean doesn't accept this lemma as a `simp` lemma? -/ +lemma arrow_congr_comp_apply {α₁ β₁ γ₁ α₂ β₂ γ₂ : Sort*} + (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (ec : γ₁ ≃ γ₂) (f : α₁ → β₁) (g : β₁ → γ₁) (x : α₂) : + arrow_congr ea ec (g ∘ f) x = arrow_congr eb ec g (arrow_congr ea eb f x) := +by simp only [arrow_congr_apply, eb.symm_apply_apply] -lemma arrow_congr_refl {α β : Sort*} : +@[simp] lemma arrow_congr_refl {α β : Sort*} : arrow_congr (equiv.refl α) (equiv.refl β) = equiv.refl (α → β) := rfl -lemma arrow_congr_trans {α₁ β₁ α₂ β₂ α₃ β₃ : Sort*} +@[simp] lemma arrow_congr_trans {α₁ β₁ α₂ β₂ α₃ β₃ : Sort*} (e₁ : α₁ ≃ α₂) (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃) : - (arrow_congr e₁ e₁').trans (arrow_congr e₂ e₂') = arrow_congr (e₁.trans e₂) (e₁'.trans e₂') := + arrow_congr (e₁.trans e₂) (e₁'.trans e₂') = (arrow_congr e₁ e₁').trans (arrow_congr e₂ e₂') := rfl -lemma arrow_congr_symm {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : +@[simp] lemma arrow_congr_symm {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : (arrow_congr e₁ e₂).symm = arrow_congr e₁.symm e₂.symm := rfl def conj (e : α ≃ β) : (α → α) ≃ (β → β) := arrow_congr e e -lemma conj_refl : conj (equiv.refl α) = equiv.refl (α → α) := rfl +@[simp] lemma conj_refl : conj (equiv.refl α) = equiv.refl (α → α) := rfl -lemma conj_symm (e : α ≃ β) : e.symm.conj = e.conj.symm := rfl +@[simp] lemma conj_symm (e : α ≃ β) : e.conj.symm = e.symm.conj := rfl -lemma conj_trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : +@[simp] lemma conj_trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : (e₁.trans e₂).conj = e₁.conj.trans e₂.conj := rfl -lemma conj_apply (e : α ≃ β) (f : α → α) : e.conj f = e.to_fun ∘ f ∘ e.inv_fun := +@[simp] lemma conj_apply (e : α ≃ β) (f : α → α) (x : β) : + e.conj f x = (e $ f $ e.inv_fun x) := rfl -lemma conj_comp_apply (e : α ≃ β) (f₁ f₂ : α → α) (y : β) : +@[simp] lemma conj_comp_apply (e : α ≃ β) (f₁ f₂ : α → α) (y : β) : e.conj (f₁ ∘ f₂) y = e.conj f₁ (e.conj f₂ y) := by apply arrow_congr_comp_apply From 5ac360b4a5621ca53df35a29ab68527d05607396 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Mon, 1 Jul 2019 15:47:45 +0300 Subject: [PATCH 3/3] Reorder, drop TODO --- src/data/equiv/basic.lean | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean index 51dd1420b6ee1..7d32cb44c413a 100644 --- a/src/data/equiv/basic.lean +++ b/src/data/equiv/basic.lean @@ -224,11 +224,10 @@ protected def plift : plift α ≃ α := arrow_congr e₁ e₂ f x = (e₂ $ f $ e₁.symm x) := rfl -/- TODO: why Lean doesn't accept this lemma as a `simp` lemma? -/ -lemma arrow_congr_comp_apply {α₁ β₁ γ₁ α₂ β₂ γ₂ : Sort*} - (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (ec : γ₁ ≃ γ₂) (f : α₁ → β₁) (g : β₁ → γ₁) (x : α₂) : - arrow_congr ea ec (g ∘ f) x = arrow_congr eb ec g (arrow_congr ea eb f x) := -by simp only [arrow_congr_apply, eb.symm_apply_apply] +lemma arrow_congr_comp {α₁ β₁ γ₁ α₂ β₂ γ₂ : Sort*} + (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (ec : γ₁ ≃ γ₂) (f : α₁ → β₁) (g : β₁ → γ₁) : + arrow_congr ea ec (g ∘ f) = (arrow_congr eb ec g) ∘ (arrow_congr ea eb f) := +by ext; simp only [comp, arrow_congr_apply, eb.symm_apply_apply] @[simp] lemma arrow_congr_refl {α β : Sort*} : arrow_congr (equiv.refl α) (equiv.refl β) = equiv.refl (α → β) := rfl @@ -244,6 +243,10 @@ rfl def conj (e : α ≃ β) : (α → α) ≃ (β → β) := arrow_congr e e +@[simp] lemma conj_apply (e : α ≃ β) (f : α → α) (x : β) : + e.conj f x = (e $ f $ e.symm x) := +rfl + @[simp] lemma conj_refl : conj (equiv.refl α) = equiv.refl (α → α) := rfl @[simp] lemma conj_symm (e : α ≃ β) : e.conj.symm = e.symm.conj := rfl @@ -252,13 +255,9 @@ def conj (e : α ≃ β) : (α → α) ≃ (β → β) := arrow_congr e e (e₁.trans e₂).conj = e₁.conj.trans e₂.conj := rfl -@[simp] lemma conj_apply (e : α ≃ β) (f : α → α) (x : β) : - e.conj f x = (e $ f $ e.inv_fun x) := -rfl - -@[simp] lemma conj_comp_apply (e : α ≃ β) (f₁ f₂ : α → α) (y : β) : - e.conj (f₁ ∘ f₂) y = e.conj f₁ (e.conj f₂ y) := -by apply arrow_congr_comp_apply +@[simp] lemma conj_comp (e : α ≃ β) (f₁ f₂ : α → α) : + e.conj (f₁ ∘ f₂) = (e.conj f₁) ∘ (e.conj f₂) := +by apply arrow_congr_comp def punit_equiv_punit : punit.{v} ≃ punit.{w} := ⟨λ _, punit.star, λ _, punit.star, λ u, by cases u; refl, λ u, by cases u; reflexivity⟩