feat(logic/equiv/set): equivalences between all preimages gives an eq…

…uivalence of domains (#13853)





Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/data/fintype/card.lean

@@ -213,7 +213,7 @@ lemma fintype.prod_fiberwise [fintype α] [decidable_eq β] [fintype β] [comm_m
   (f : α → β) (g : α → γ) :
   (∏ b : β, ∏ a : {a // f a = b}, g (a : α)) = ∏ a, g a :=
 begin
-  rw [← (equiv.sigma_preimage_equiv f).prod_comp, ← univ_sigma_univ, prod_sigma],
+  rw [← (equiv.sigma_fiber_equiv f).prod_comp, ← univ_sigma_univ, prod_sigma],
   refl
 end
 

src/group_theory/coset.lean

@@ -383,7 +383,7 @@ def right_coset_equiv_subgroup (g : α) : right_coset ↑s g ≃ s :=
 noncomputable def group_equiv_quotient_times_subgroup :
   α ≃ (α ⧸ s) × s :=
 calc α ≃ Σ L : α ⧸ s, {x : α // (x : α ⧸ s) = L} :
-  (equiv.sigma_preimage_equiv quotient_group.mk).symm
+  (equiv.sigma_fiber_equiv quotient_group.mk).symm
     ... ≃ Σ L : α ⧸ s, left_coset (quotient.out' L) s :
   equiv.sigma_congr_right (λ L,
     begin

src/group_theory/group_action/basic.lean

@@ -243,7 +243,7 @@ as a special case."]
 def self_equiv_sigma_orbits' {φ : Ω → β} (hφ : right_inverse φ quotient.mk') :
   β ≃ Σ (ω : Ω), orbit α (φ ω) :=
 calc  β
-    ≃ Σ (ω : Ω), {b // quotient.mk' b = ω} : (equiv.sigma_preimage_equiv quotient.mk').symm
+    ≃ Σ (ω : Ω), {b // quotient.mk' b = ω} : (equiv.sigma_fiber_equiv quotient.mk').symm
 ... ≃ Σ (ω : Ω), orbit α (φ ω) :
         equiv.sigma_congr_right (λ ω, equiv.subtype_equiv_right $
           λ x, by {rw [← hφ ω, quotient.eq', hφ ω], refl })

src/group_theory/p_group.lean

@@ -121,7 +121,7 @@ lemma card_modeq_card_fixed_points : card α ≡ card (fixed_points G α) [MOD p
 begin
   classical,
   calc card α = card (Σ y : quotient (orbit_rel G α), {x // quotient.mk' x = y}) :
-    card_congr (equiv.sigma_preimage_equiv (@quotient.mk' _ (orbit_rel G α))).symm
+    card_congr (equiv.sigma_fiber_equiv (@quotient.mk' _ (orbit_rel G α))).symm
   ... = ∑ a : quotient (orbit_rel G α), card {x // quotient.mk' x = a} : card_sigma _
   ... ≡ ∑ a : fixed_points G α, 1 [MOD p] : _
   ... = _ : by simp; refl,

src/logic/equiv/basic.lean

@@ -778,10 +778,11 @@ def sum_equiv_sigma_bool (α β : Type u) : α ⊕ β ≃ (Σ b: bool, cond b α
  λ s, by cases s; refl,
  λ s, by rcases s with ⟨_|_, _⟩; refl⟩
 
-/-- `sigma_preimage_equiv f` for `f : α → β` is the natural equivalence between
+/-- `sigma_fiber_equiv f` for `f : α → β` is the natural equivalence between
 the type of all fibres of `f` and the total space `α`. -/
+-- See also `equiv.sigma_preimage_equiv`.
 @[simps]
-def sigma_preimage_equiv {α β : Type*} (f : α → β) :
+def sigma_fiber_equiv {α β : Type*} (f : α → β) :
   (Σ y : β, {x // f x = y}) ≃ α :=
 ⟨λ x, ↑x.2, λ x, ⟨f x, x, rfl⟩, λ ⟨y, x, rfl⟩, rfl, λ x, rfl⟩
 
@@ -1119,6 +1120,18 @@ lemma sigma_equiv_prod_sigma_congr_right :
     (prod_congr_right e).trans (sigma_equiv_prod α₁ β₂).symm :=
 by { ext ⟨a, b⟩ : 1, simp }
 
+/-- A family of equivalences between fibers gives an equivalence between domains. -/
+-- See also `equiv.of_preimage_equiv`.
+@[simps]
+def of_fiber_equiv {α β γ : Type*} {f : α → γ} {g : β → γ}
+  (e : Π c, {a // f a = c} ≃ {b // g b = c}) :
+  α ≃ β :=
+(sigma_fiber_equiv f).symm.trans $ (equiv.sigma_congr_right e).trans (sigma_fiber_equiv g)
+
+lemma of_fiber_equiv_map {α β γ} {f : α → γ} {g : β → γ}
+  (e : Π c, {a // f a = c} ≃ {b // g b = c}) (a : α) : g (of_fiber_equiv e a) = f a :=
+(_ : {b // g b = _}).prop
+
 /-- A variation on `equiv.prod_congr` where the equivalence in the second component can depend
   on the first component. A typical example is a shear mapping, explaining the name of this
   declaration. -/
@@ -1409,15 +1422,15 @@ def sigma_subtype_equiv_of_subset {α : Type u} (p : α → Type v) (q : α →
 
 /-- If a predicate `p : β → Prop` is true on the range of a map `f : α → β`, then
 `Σ y : {y // p y}, {x // f x = y}` is equivalent to `α`. -/
-def sigma_subtype_preimage_equiv {α : Type u} {β : Type v} (f : α → β) (p : β → Prop)
+def sigma_subtype_fiber_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
+   ... ≃ α                           : sigma_fiber_equiv f
 
 /-- If for each `x` we have `p x ↔ q (f x)`, then `Σ y : {y // q y}, f ⁻¹' {y}` is equivalent
 to `{x // p x}`. -/
-def sigma_subtype_preimage_equiv_subtype {α : Type u} {β : Type v} (f : α → β)
+def sigma_subtype_fiber_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}) ≃
@@ -1430,8 +1443,7 @@ calc (Σ y : subtype q, {x : α // f x = y}) ≃
     assume x,
     exact ⟨λ ⟨hp, h'⟩, congr_arg subtype.val h', λ h', ⟨(h x).2 (h'.symm ▸ y.2), subtype.eq h'⟩⟩
   end
-
-   ... ≃ subtype p : sigma_preimage_equiv (λ x : subtype p, (⟨f x, (h x).1 x.property⟩ : subtype q))
+   ... ≃ subtype p : sigma_fiber_equiv (λ x : subtype p, (⟨f x, (h x).1 x.property⟩ : subtype q))
 
 /-- A sigma type over an `option` is equivalent to the sigma set over the original type,
 if the fiber is empty at none. -/

src/logic/equiv/set.lean

@@ -512,6 +512,23 @@ begin
   by_cases hi : p i; simp [hi]
 end
 
+/-- `sigma_fiber_equiv f` for `f : α → β` is the natural equivalence between
+the type of all preimages of points under `f` and the total space `α`. -/
+-- See also `equiv.sigma_fiber_equiv`.
+@[simps] def sigma_preimage_equiv {α β} (f : α → β) : (Σ b, f ⁻¹' {b}) ≃ α :=
+sigma_fiber_equiv f
+
+/-- A family of equivalences between preimages of points gives an equivalence between domains. -/
+-- See also `equiv.of_fiber_equiv`.
+@[simps]
+def of_preimage_equiv {α β γ} {f : α → γ} {g : β → γ} (e : Π c, (f ⁻¹' {c}) ≃ (g ⁻¹' {c})) :
+  α ≃ β :=
+equiv.of_fiber_equiv e
+
+lemma of_preimage_equiv_map {α β γ} {f : α → γ} {g : β → γ}
+  (e : Π c, (f ⁻¹' {c}) ≃ (g ⁻¹' {c})) (a : α) : g (of_preimage_equiv e a) = f a :=
+equiv.of_fiber_equiv_map e a
+
 end equiv
 
 /-- If a function is a bijection between two sets `s` and `t`, then it induces an

src/logic/small.lean

@@ -136,7 +136,7 @@ small_of_injective (equiv.vector_equiv_fin α n).injective
 instance small_list {α : Type v} [small.{u} α] :
   small.{u} (list α) :=
 begin
-  let e : (Σ n, vector α n) ≃ list α := equiv.sigma_preimage_equiv list.length,
+  let e : (Σ n, vector α n) ≃ list α := equiv.sigma_fiber_equiv list.length,
   exact small_of_surjective e.surjective,
 end
 

src/set_theory/cardinal/basic.lean

@@ -636,7 +636,7 @@ theorem sum_le_sum {ι} (f g : ι → cardinal) (H : ∀ i, f i ≤ g i) : sum f
 
 lemma mk_le_mk_mul_of_mk_preimage_le {c : cardinal} (f : α → β) (hf : ∀ b : β, #(f ⁻¹' {b}) ≤ c) :
   #α ≤ #β * c :=
-by simpa only [←mk_congr (@equiv.sigma_preimage_equiv α β f), mk_sigma, ←sum_const']
+by simpa only [←mk_congr (@equiv.sigma_fiber_equiv α β f), mk_sigma, ←sum_const']
   using sum_le_sum _ _ hf
 
 /-- The range of an indexed cardinal function, whose outputs live in a higher universe than the
@@ -1282,7 +1282,7 @@ mk_eq_one _
 (mk_congr (equiv.vector_equiv_fin α n)).trans $ by simp
 
 theorem mk_list_eq_sum_pow (α : Type u) : #(list α) = sum (λ n : ℕ, (#α) ^ℕ n) :=
-calc #(list α) = #(Σ n, vector α n) : mk_congr (equiv.sigma_preimage_equiv list.length).symm
+calc #(list α) = #(Σ n, vector α n) : mk_congr (equiv.sigma_fiber_equiv list.length).symm
 ... = sum (λ n : ℕ, (#α) ^ℕ n) : by simp
 
 theorem mk_quot_le {α : Type u} {r : α → α → Prop} : #(quot r) ≤ #α :=