feat(data/equiv/basic): add more functions for equivalences between c…

…omplex types (#1384)

* Add more `equiv` combinators

* Fix compile

* Minor fixes

* Update src/data/equiv/basic.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

src/data/equiv/basic.lean

@@ -404,9 +404,9 @@ def sum_equiv_sigma_bool (α β : Sort*) : α ⊕ β ≃ (Σ b: bool, cond b α
  λ s, by cases s; refl,
  λ s, by rcases s with ⟨_|_, _⟩; refl⟩
 
-def equiv_fib {α β : Type*} (f : α → β) :
-  α ≃ Σ y : β, {x // f x = y} :=
-⟨λ x, ⟨f x, x, rfl⟩, λ x, x.2.1, λ x, rfl, λ ⟨y, x, rfl⟩, rfl⟩
+def sigma_preimage_equiv {α β : Type*} (f : α → β) :
+  (Σ y : β, {x // f x = y}) ≃ α :=
+⟨λ x, x.2.1, λ x, ⟨f x, x, rfl⟩, λ ⟨y, x, rfl⟩, rfl, λ x, rfl⟩
 
 end
 
@@ -563,26 +563,68 @@ subtype_congr (equiv.refl α) (assume a, h ▸ iff.refl _)
 def set_congr {α : Type*} {s t : set α} (h : s = t) : s ≃ t :=
 subtype_congr_prop h
 
-def subtype_subtype_equiv_subtype {α : Type u} (p : α → Prop) (q : subtype p → Prop) :
+def subtype_subtype_equiv_subtype_exists {α : Type u} (p : α → Prop) (q : subtype p → Prop) :
   subtype q ≃ {a : α // ∃h:p a, q ⟨a, h⟩ } :=
 ⟨λ⟨⟨a, ha⟩, ha'⟩, ⟨a, ha, ha'⟩,
   λ⟨a, ha⟩, ⟨⟨a, ha.cases_on $ assume h _, h⟩, by { cases ha, exact ha_h }⟩,
   assume ⟨⟨a, ha⟩, h⟩, rfl, assume ⟨a, h₁, h₂⟩, rfl⟩
 
-/- A subtype of a sigma-type is a sigma-type over a subtype. -/
+def subtype_subtype_equiv_subtype_inter {α : Type u} (p q : α → Prop) :
+  {x : subtype p // q x.1} ≃ subtype (λ x, p x ∧ q x) :=
+(subtype_subtype_equiv_subtype_exists p _).trans $
+subtype_congr_right $ λ x, exists_prop
+
+/-- If the outer subtype has more restrictive predicate than the inner one,
+then we can drop the latter. -/
+def subtype_subtype_equiv_subtype {α : Type u} {p q : α → Prop} (h : ∀ {x}, q x → p x) :
+  {x : subtype p // q x.1} ≃ subtype q :=
+(subtype_subtype_equiv_subtype_inter p _).trans $
+subtype_congr_right $
+assume x,
+⟨and.right, λ h₁, ⟨h h₁, h₁⟩⟩
+
+/-- If a proposition holds for all elements, then the subtype is
+equivalent to the original type. -/
+def subtype_univ_equiv {α : Type u} {p : α → Prop} (h : ∀ x, p x) :
+  subtype p ≃ α :=
+⟨λ x, x, λ x, ⟨x, h x⟩, λ x, subtype.eq rfl, λ x, rfl⟩
+
+/-- A subtype of a sigma-type is a sigma-type over a subtype. -/
 def subtype_sigma_equiv {α : Type u} (p : α → Type v) (q : α → Prop) :
   { y : sigma p // q y.1 } ≃ Σ(x : subtype q), p x.1 :=
-begin
-  fsplit,
-  rintro ⟨⟨x, y⟩, z⟩, exact ⟨⟨x, z⟩, y⟩,
-  rintro ⟨⟨x, y⟩, z⟩, exact ⟨⟨x, z⟩, y⟩,
-  rintro ⟨⟨x, y⟩, z⟩, refl,
-  rintro ⟨⟨x, y⟩, z⟩, refl,
-end
+⟨λ x, ⟨⟨x.1.1, x.2⟩, x.1.2⟩,
+ λ x, ⟨⟨x.1.1, x.2⟩, x.1.2⟩,
+ λ ⟨⟨x, h⟩, y⟩, rfl,
+ λ ⟨⟨x, y⟩, h⟩, rfl⟩
+
+/-- A sigma type over a subtype is equivalent to the sigma set over the original type,
+if the fiber is empty outside of the subset -/
+def sigma_subtype_equiv_of_subset {α : Type u} (p : α → Type v) (q : α → Prop)
+  (h : ∀ x, p x → q x) :
+  (Σ x : subtype q, p x) ≃ Σ x : α, p x :=
+(subtype_sigma_equiv p q).symm.trans $ subtype_univ_equiv $ λ x, h x.1 x.2
+
+def sigma_subtype_preimage_equiv {α : Type u} {β : Type v} (f : α → β) (p : β → Prop)
+  (h : ∀ x, p (f x)) :
+  (Σ y : subtype p, {x : α // f x = y}) ≃ α :=
+calc _ ≃ Σ y : β, {x : α // f x = y} : sigma_subtype_equiv_of_subset _ p (λ y ⟨x, h'⟩, h' ▸ h x)
+   ... ≃ α                           : sigma_preimage_equiv f
+
+def sigma_subtype_preimage_equiv_subtype {α : Type u} {β : Type v} (f : α → β)
+  {p : α → Prop} {q : β → Prop} (h : ∀ x, p x ↔ q (f x)) :
+  (Σ y : subtype q, {x : α // f x = y}) ≃ subtype p :=
+calc (Σ y : subtype q, {x : α // f x = y}) ≃
+  Σ y : subtype q, {x : subtype p // subtype.mk (f x) ((h x).1 x.2) = y} :
+  begin
+    apply sigma_congr_right,
+    assume y,
+    symmetry,
+    refine (subtype_subtype_equiv_subtype_exists _ _).trans (subtype_congr_right _),
+    assume x,
+    exact ⟨λ ⟨hp, h'⟩, congr_arg subtype.val h', λ h', ⟨(h x).2 (h'.symm ▸ y.2), subtype.eq h'⟩⟩
+  end
 
-/-- aka coimage -/
-def equiv_sigma_subtype {α : Type u} {β : Type v} (f : α → β) : α ≃ Σ b, {x : α // f x = b} :=
-⟨λ x, ⟨f x, x, rfl⟩, λ x, x.2.1, λ x, rfl, λ ⟨b, x, H⟩, sigma.eq H $ eq.drec_on H $ subtype.eq rfl⟩
+   ... ≃ subtype p : sigma_preimage_equiv (λ x : subtype p, (⟨f x, (h x).1 x.property⟩ : subtype q))
 
 def pi_equiv_subtype_sigma (ι : Type*) (π : ι → Type*) :
   (Πi, π i) ≃ {f : ι → Σi, π i | ∀i, (f i).1 = i } :=
@@ -757,10 +799,7 @@ protected def congr {α β : Type*} (e : α ≃ β) : set α ≃ set β :=
 
 protected def sep {α : Type u} (s : set α) (t : α → Prop) :
   ({ x ∈ s | t x } : set α) ≃ { x : s | t x.1 } :=
-begin
-  symmetry, apply (equiv.subtype_subtype_equiv_subtype _ _).trans _,
-  simp only [mem_set_of_eq, exists_prop], refl
-end
+(equiv.subtype_subtype_equiv_subtype_inter s t).symm
 
 end set
 

src/group_theory/coset.lean

@@ -207,7 +207,7 @@ def left_coset_equiv_subgroup (g : α) : left_coset g s ≃ s :=
 noncomputable def group_equiv_quotient_times_subgroup (hs : is_subgroup s) :
   α ≃ quotient s × s :=
 calc α ≃ Σ L : quotient s, {x : α // (x : quotient s)= L} :
-  equiv.equiv_fib quotient_group.mk
+  (equiv.sigma_preimage_equiv quotient_group.mk).symm
     ... ≃ Σ L : quotient s, left_coset (quotient.out' L) s :
   equiv.sigma_congr_right (λ L,
     begin rw ← eq_class_eq_left_coset,

src/group_theory/sylow.lean

@@ -31,7 +31,7 @@ end
 lemma card_modeq_card_fixed_points [fintype α] [fintype G] [fintype (fixed_points G α)]
   {p n : ℕ} (hp : nat.prime p) (h : card G = p ^ n) : card α ≡ card (fixed_points G α) [MOD p] :=
 calc card α = card (Σ y : quotient (orbit_rel G α), {x // quotient.mk' x = y}) :
-  card_congr (equiv_fib (@quotient.mk' _ (orbit_rel G α)))
+  card_congr (sigma_preimage_equiv (@quotient.mk' _ (orbit_rel G α))).symm
 ... = univ.sum (λ a : quotient (orbit_rel G α), card {x // quotient.mk' x = a}) : card_sigma _
 ... ≡ (@univ (fixed_points G α) _).sum (λ _, 1) [MOD p] :
 begin

src/set_theory/cardinal.lean

@@ -778,7 +778,7 @@ quotient.sound ⟨equiv.option_equiv_sum_punit α⟩
 
 theorem mk_list_eq_sum_pow (α : Type u) : mk (list α) = sum (λ n : ℕ, (mk α)^(n:cardinal.{u})) :=
 calc  mk (list α)
-    = mk (Σ n, vector α n) : quotient.sound ⟨equiv.equiv_sigma_subtype list.length⟩
+    = mk (Σ n, vector α n) : quotient.sound ⟨(equiv.sigma_preimage_equiv list.length).symm⟩
 ... = mk (Σ n, fin n → α) : quotient.sound ⟨equiv.sigma_congr_right $ λ n,
   ⟨vector.nth, vector.of_fn, vector.of_fn_nth, λ f, funext $ vector.nth_of_fn f⟩⟩
 ... = mk (Σ n : ℕ, ulift.{u} (fin n) → α) : quotient.sound ⟨equiv.sigma_congr_right $ λ n,

src/set_theory/cofinality.lean

@@ -400,7 +400,7 @@ begin
   refine ⟨a, {x | ∃(h : x ∈ s), f ⟨x, h⟩ = a}, _, _, _⟩,
   { rintro x ⟨hx, hx'⟩, exact hx },
   { refine le_trans ha _, apply ge_of_eq, apply quotient.sound, constructor,
-    refine equiv.trans _ (equiv.subtype_subtype_equiv_subtype _ _).symm,
+    refine equiv.trans _ (equiv.subtype_subtype_equiv_subtype_exists _ _).symm,
     simp only [set_coe_eq_subtype, mem_singleton_iff, mem_preimage, mem_set_of_eq] },
   rintro x ⟨hx, hx'⟩, exact hx'
 end