Zulip Chat Archive

Stream: general

Topic: equiv.pi_congr_left

Scott Morrison (Mar 21 2020 at 05:31):

Is this even provable?

import data.equiv.basic

universes u₁ u₂ u₃

def equiv.pi_congr_left {α : Sort u₁} {β : Sort u₂} (P : α → Sort u₃) (e : α ≃ β) :
  (Π a, P a) ≃ (Π b, P (e.symm b)) :=
sorry

Scott Morrison (Mar 21 2020 at 05:34):

or perhaps since it's not even true in topological spaces, I shouldn't expect to prove it in dependent type theory??

Scott Morrison (Mar 21 2020 at 05:36):

def equiv.forall_congr_left {α : Sort u₁} {β : Sort u₂} (P : α → Prop) (e : α ≃ β) : (∀ a, P a) ↔ (∀ b, P (e.symm b)) :=
{ mp := λ f b, f (e.symm b),
  mpr := λ g a, begin convert g _, swap, exact e a, simp, end, }

is perfectly okay.

Yury G. Kudryashov (Mar 21 2020 at 05:45):

(deleted)

Yury G. Kudryashov (Mar 21 2020 at 05:47):

def equiv.pi_congr_left {α : Sort u} {β : Sort v} (P : α → Sort w) (e : α ≃ β) :
  (Π a, P a) ≃ (Π b, P (e.symm b)) :=
{ to_fun := λ f x, f (e.symm x),
  inv_fun := λ f x, begin rw [← e.symm_apply_apply x], exact f (e x)  end,
  left_inv := λ f, begin ext x, simp only [], apply eq_of_heq, refine heq.trans (eq_rec_heq _ _) _, rw [e.symm_apply_apply]  end,
  right_inv := λ f, begin ext x, simp only [], apply eq_of_heq, refine heq.trans (eq_rec_heq _ _) _, rw e.apply_symm_apply end }

Yury G. Kudryashov (Mar 21 2020 at 05:48):

(probably needs style tweaks before submitting a PR)

Scott Morrison (Mar 21 2020 at 05:57):

Slightly golfed:

def equiv.pi_congr_left {α : Sort u} {β : Sort v} (P : α → Sort w) (e : α ≃ β) :
  (Π a, P a) ≃ (Π b, P (e.symm b)) :=
{ to_fun := λ f x, f (e.symm x),
  inv_fun := λ f x, begin rw [← e.symm_apply_apply x], exact f (e x)  end,
  left_inv := λ f, funext $ λ x, eq_of_heq (heq.trans (eq_rec_heq _ _) (by { dsimp, rw [e.symm_apply_apply] })),
  right_inv := λ f, funext $ λ x, eq_of_heq (heq.trans (eq_rec_heq _ _) (by { rw e.apply_symm_apply })) }

Scott Morrison (Mar 21 2020 at 06:12):

@Yury G. Kudryashov, do you know how to turn eq.mpr into eq.rec_on?

Scott Morrison (Mar 21 2020 at 06:12):

Usually my instinct is that this is the bad direction, but to follow your proof in another situation I now want it!

Scott Morrison (Mar 21 2020 at 06:21):

Think I've got it.

Scott Morrison (Mar 21 2020 at 06:38):

And here's the "full" version:

universes u₁ u₂ u₃ u₄

def equiv.pi_congr {α : Sort u₁} {β : Sort u₂}
  (W : α → Sort u₃) (Z : β → Sort u₄) (h₁ : α ≃ β) (h₂ : Π a : α, (W a ≃ Z (h₁ a))) : (Π a, W a) ≃ (Π b, Z b) :=
{ to_fun := λ f b, by { rw ← h₁.apply_symm_apply b, exact h₂ (h₁.symm b) (f (h₁.symm b)), },
  inv_fun := λ g a, (h₂ a).symm (g (h₁ a)),
  left_inv := λ f, funext $ λ a,
  begin
    rw ←(h₂ a).symm_apply_apply (f a),
    dsimp,
    exact congr_arg _ (eq_of_heq ((eq_rec_heq _ _).trans (by rw h₁.symm_apply_apply))),
  end,
  right_inv := λ g, funext $ λ b,
    eq_of_heq ((eq_rec_heq _ _).trans (by { rw (h₂ (h₁.symm b)).apply_symm_apply, congr, simp, })), }

Mario Carneiro (Mar 21 2020 at 07:49):

here's a heq-less proof:

def equiv.pi_congr_left {α : Sort u} {β : Sort v} (P : β → Sort w) (e : α ≃ β) :
  (Π a, P (e a)) ≃ (Π b, P b) :=
{ to_fun := λ f x, (e.apply_symm_apply x).rec_on (f (e.symm x)),
  inv_fun := λ f x, f (e x),
  left_inv := λ f, funext $ λ x,
    (by rintro _ rfl; refl : ∀ {y} h, (congr_arg e h).rec_on (f y) = f x) (e.symm_apply_apply x),
  right_inv := λ f, funext $ λ x,
    (by rintro _ rfl; refl : ∀ {y} (h : y = x), h.rec_on (f y) = f x) (e.apply_symm_apply x) }

Mario Carneiro (Mar 21 2020 at 07:55):

or with match:

def equiv.pi_congr_left {α : Sort u} {β : Sort v} (P : β → Sort w) (e : α ≃ β) :
  (Π a, P (e a)) ≃ (Π b, P b) :=
{ to_fun := λ f x, (e.apply_symm_apply x).rec_on (f (e.symm x)),
  inv_fun := λ f x, f (e x),
  left_inv := λ f, funext $ λ x,
    match _, e.symm_apply_apply x : ∀ {y} (h : y = x), (congr_arg e h).rec_on (f y) = f x with rfl := rfl end,
  right_inv := λ f, funext $ λ x,
    match _, e.apply_symm_apply x : ∀ {y} (h : y = x), h.rec_on (f y) = f x with rfl := rfl end }

Mario Carneiro (Mar 21 2020 at 08:03):

However, pi_congr is easy given these two lemmas:

def equiv.pi_congr {α β} (W : α → Sort*) (Z : β → Sort*)
  (e₁ : α ≃ β) (e₂ : Π a : α, W a ≃ Z (e₁ a)) : (Π a, W a) ≃ (Π b, Z b) :=
(equiv.Pi_congr_right e₂).trans (equiv.pi_congr_left _ e₁)

Kevin Buzzard (Mar 21 2020 at 08:04):

If it's any consolation, it was already trivial in maths ;-)

Mario Carneiro (Mar 21 2020 at 08:05):

the reason I didn't prove this in the first place is because the statement looks too difficult to use well

Mario Carneiro (Mar 21 2020 at 08:06):

The capitalization on Pi is inconsistent here

Scott Morrison (Mar 21 2020 at 08:12):

cool!

Scott Morrison (Mar 21 2020 at 08:19):

oh, actually... I don't like the statement of pi_congr_left as much as the previous ones. That is, I think (Π a, P a) ≃ (Π b, P (e.symm b)) is the more natural conclusion.

Scott Morrison (Mar 21 2020 at 08:20):

do you have a strong opinion about what should be in the library?

Scott Morrison (Mar 21 2020 at 08:22):

I just want to think of it as: given an equivalence that turns α into β, what does Π a, P a turn into? And so I want the equivalence showing up only on the right hand side.

Mario Carneiro (Mar 21 2020 at 08:41):

It is very important that the statement of the theorem use e and not e.symm

Scott Morrison (Mar 21 2020 at 08:41):

why is that?

Mario Carneiro (Mar 21 2020 at 08:41):

because an arbitrary equivalence is not always defeq to some e.symm

Mario Carneiro (Mar 21 2020 at 08:42):

this is why you can prove pi_congr using my version of pi_congr_left but not yours

Kevin Buzzard (Mar 21 2020 at 08:42):

Really? Is e.symm.symm not defeq to e?

Mario Carneiro (Mar 21 2020 at 08:42):

no, that is impossible to arrange

Mario Carneiro (Mar 21 2020 at 08:43):

it is possible to make it defeq up to eta expanding e, meaning that it will be defeq for any concrete function, but not given a variable

Scott Morrison (Mar 21 2020 at 08:43):

def Pi_congr_left : (Π a, P a) ≃ (Π b, P (e.symm b)) := ...

def Pi_congr : (Π a, W a) ≃ (Π b, Z b) :=
(equiv.Pi_congr_right h₂).trans (equiv.Pi_congr_left _ h₁.symm).symm