a fact about equivalences built fiber-wise

Stream: Is there code for X?

[Yaël Dillies]

Having a go. Looks like some category constructions.

[Yaël Dillies]

Hmmm... progress, somewhat?

def equiv_of_preimage_equiv {α β γ : Type*} (f : α → γ) (g : β → γ)
  (e : Π c, (f ⁻¹' {c}) ≃ (g ⁻¹' {c})) : {e : α ≃ β // ∀ a, g (e a) = f a} :=
begin
  have h : ∀ a, g (e (f a) ⟨a, rfl⟩) = f a := λ a, (e (f a) ⟨a, rfl⟩).2,
  refine ⟨⟨_, _, _, _⟩, _⟩,
  { intro a, exact (e (f a) ⟨a, rfl⟩).1 },
  { intro b, exact ((e $ g b).symm ⟨b, rfl⟩).1 },
  { intro a,
    dsimp,
    refine eq.trans _ (congr_arg coe $ (e $ f a).symm_apply_apply ⟨a, rfl⟩),
    convert congr_fun_heq _ _ _, swap,
    refine congr_arg subtype _,
    simp_rw h,
    sorry
  },
end

[Yaël Dillies]

There's also docs#subtype.heq_iff_coe_eq which might be useful.

[Scott Morrison]

Aha!

[Scott Morrison]

import data.set.basic

@[simps]
def preimage_congr {α γ : Type*} (f : α → γ)
  {c c' : γ} (h : c = c') : f ⁻¹' {c} ≃ f ⁻¹' {c'} :=
{ to_fun := λ x, ⟨x.1, by simpa [h] using x.2⟩,
  inv_fun := λ x, ⟨x.1, by simpa [h] using x.2⟩,
  left_inv := λ x, by simp,
  right_inv := λ x, by simp, }

lemma preimage_congr_lemma {α β γ : Type*} {f : α → γ} {g : β → γ} (e : Π c, (f ⁻¹' {c}) ≃ (g ⁻¹' {c}))
  {c c' : γ} (h : c = c') (x : f ⁻¹' {c}) :
  e c x = (preimage_congr g h.symm) (e c' ⟨x.1, begin simpa [h] using x.2, end⟩) :=
begin
  ext, simp, cases h, simp,
end

def equiv_of_preimage_equiv
  {α β γ : Type*} (f : α → γ) (g : β → γ) (e : Π c, (f ⁻¹' {c}) ≃ (g ⁻¹' {c})) :
  { e : α ≃ β // ∀ a, g (e a) = f a } :=
begin
  have h : ∀ a, g (e (f a) ⟨a, (by simp)⟩).val = f a := λ a, (e (f a) ⟨a, (by simp)⟩).2,
  have h' : ∀ b, f ((e (g b)).symm ⟨b, (by simp)⟩).val = g b := λ b, ((e (g b)).symm ⟨b, (by simp)⟩).2,
  refine ⟨⟨_, _, _, _⟩, _⟩,
  { intro a, exact (e (f a) ⟨a, (by simp)⟩).1, },
  { intro b, exact ((e (g b)).symm ⟨b, (by simp)⟩).1, },
  { intro a,
    simp only [preimage_congr_lemma e (h a).symm],
    simp, },
  { intro b,
    have := (e (g b)).apply_symm_apply ⟨b, (by simp)⟩,
    simp only [preimage_congr_lemma e (h' b)],
    simp, },
  { simpa using h, },
end

[Scott Morrison]

golfed a bit and PR's as #13853. Thanks for the help!

[Junyan Xu]

This is a better way to refactor it IMO:

import data.set.basic

variables {α α' β : Type*} (f : α → β) {g : α' → β}

@[simps] def domain_equiv_psigma_fiber : α ≃ psigma (λ b, f ⁻¹' {b}) :=
{ to_fun := λ a, ⟨f a, a, rfl⟩,
  inv_fun := λ a, a.2.1,
  left_inv := λ a, rfl,
  right_inv := λ ⟨a,b,rfl⟩, rfl }

variable {f}
def equiv_of_fiber_equiv (e : Π c, (f ⁻¹' {c}) ≃ (g ⁻¹' {c})) : α ≃ α' :=
(domain_equiv_psigma_fiber f).trans $ (equiv.psigma_congr_right e).trans (domain_equiv_psigma_fiber g).symm

Do we really not have domain_equiv_psigma_fiber?

[Scott Morrison]

I've updated the PR to use this version, thank you!

[Scott Morrison]

I also regularised names slightly, using fiber to refer to {x // f x = y} and preimage to refer to f ⁻¹' {c}.