feat(*): more bundled versions of (fin 2 → α) ≃ (α × α) (#10214)

Also ensure that the inverse function uses vector notation when possible.

Author: urkud

src/data/equiv/fin.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import data.fin.basic
+import data.fin.vec_notation
 import data.equiv.basic
 import tactic.norm_num
 
@@ -54,13 +54,14 @@ non-dependent version and `prod_equiv_pi_fin_two` for a version with inputs `α
 `γ = fin.cons α (fin.cons β fin_zero_elim)`. See also `pi_fin_two_equiv` and
 `fin_two_arrow_equiv`. -/
 @[simps {fully_applied := ff }] def prod_equiv_pi_fin_two (α β : Type u) :
-  α × β ≃ Π i : fin 2, @fin.cons _ (λ _, Type u) α (fin.cons β fin_zero_elim) i :=
+  α × β ≃ Π i : fin 2, ![α, β] i :=
 (pi_fin_two_equiv (fin.cons α (fin.cons β fin_zero_elim))).symm
 
 /-- The space of functions `fin 2 → α` is equivalent to `α × α`. See also `pi_fin_two_equiv` and
 `prod_equiv_pi_fin_two`. -/
-@[simps {fully_applied := ff}] def fin_two_arrow_equiv (α : Type*) : (fin 2 → α) ≃ α × α :=
-pi_fin_two_equiv (λ _, α)
+@[simps { fully_applied := ff }] def fin_two_arrow_equiv (α : Type*) : (fin 2 → α) ≃ α × α :=
+{ inv_fun := λ x, ![x.1, x.2],
+  .. pi_fin_two_equiv (λ _, α) }
 
 /-- `Π i : fin 2, α i` is order equivalent to `α 0 × α 1`. See also `order_iso.fin_two_arrow_equiv`
 for a non-dependent version. -/
@@ -72,7 +73,7 @@ def order_iso.pi_fin_two_iso (α : fin 2 → Type u) [Π i, preorder (α i)] :
 /-- The space of functions `fin 2 → α` is order equivalent to `α × α`. See also
 `order_iso.pi_fin_two_iso`. -/
 def order_iso.fin_two_arrow_iso (α : Type*) [preorder α] : (fin 2 → α) ≃o α × α :=
-order_iso.pi_fin_two_iso (λ _, α)
+{ to_equiv := fin_two_arrow_equiv α, .. order_iso.pi_fin_two_iso (λ _, α) }
 
 /-- The 'identity' equivalence between `fin n` and `fin m` when `n = m`. -/
 def fin_congr {n m : ℕ} (h : n = m) : fin n ≃ fin m :=

src/linear_algebra/pi.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov, Eric Wieser
 -/
 import linear_algebra.basic
+import data.equiv.fin
 
 /-!
 # Pi types of modules
@@ -341,6 +342,21 @@ def fun_unique (ι R M : Type*) [unique ι] [semiring R] [add_comm_monoid M] [mo
   map_smul' := λ c f, rfl,
   .. equiv.fun_unique ι M }
 
+variables (R M)
+
+/-- Linear equivalence between dependent functions `Π i : fin 2, M i` and `M 0 × M 1`. -/
+@[simps { simp_rhs := tt, fully_applied := ff }]
+def pi_fin_two (M : fin 2 → Type v) [Π i, add_comm_monoid (M i)] [Π i, module R (M i)] :
+  (Π i, M i) ≃ₗ[R] M 0 × M 1 :=
+{ map_add' := λ f g, rfl,
+  map_smul' := λ c f, rfl,
+  .. pi_fin_two_equiv M }
+
+/-- Linear equivalence between vectors in `M² = fin 2 → M` and `M × M`. -/
+@[simps { simp_rhs := tt, fully_applied := ff }]
+def fin_two_arrow : (fin 2 → M) ≃ₗ[R] M × M :=
+{ .. fin_two_arrow_equiv M, .. pi_fin_two R (λ _, M) }
+
 end linear_equiv
 
 section extend

src/topology/algebra/module.lean

@@ -238,9 +238,7 @@ section semiring
 -/
 
 variables
-{R₁ : Type*} [semiring R₁]
-{R₂ : Type*} [semiring R₂]
-{R₃ : Type*} [semiring R₃]
+{R₁ : Type*} {R₂ : Type*} {R₃ : Type*} [semiring R₁] [semiring R₂] [semiring R₃]
 {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃}
 {M₁ : Type*} [topological_space M₁] [add_comm_monoid M₁]
 {M₂ : Type*} [topological_space M₂] [add_comm_monoid M₂]
@@ -274,6 +272,16 @@ coe_injective.eq_iff
 theorem coe_fn_injective : @function.injective (M₁ →SL[σ₁₂] M₂) (M₁ → M₂) coe_fn :=
 linear_map.coe_injective.comp coe_injective
 
+/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
+  because it is a composition of multiple projections. -/
+def simps.apply (h : M₁ →SL[σ₁₂] M₂) : M₁ → M₂ := h
+
+/-- See Note [custom simps projection]. -/
+def simps.coe (h : M₁ →SL[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂ := h
+
+initialize_simps_projections continuous_linear_map
+  (to_linear_map_to_fun → apply, to_linear_map → coe)
+
 @[ext] theorem ext {f g : M₁ →SL[σ₁₂] M₂} (h : ∀ x, f x = g x) : f = g :=
 coe_fn_injective $ funext h
 
@@ -1063,18 +1071,16 @@ namespace continuous_linear_equiv
 
 section add_comm_monoid
 
-variables {R₁ : Type*} [semiring R₁]
-{R₂ : Type*} [semiring R₂]
-{R₃ : Type*} [semiring R₃]
+variables {R₁ : Type*} {R₂ : Type*} {R₃ : Type*} [semiring R₁] [semiring R₂] [semiring R₃]
+{σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂]
+{σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [ring_hom_inv_pair σ₂₃ σ₃₂] [ring_hom_inv_pair σ₃₂ σ₂₃]
+{σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [ring_hom_inv_pair σ₁₃ σ₃₁] [ring_hom_inv_pair σ₃₁ σ₁₃]
+[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
 {M₁ : Type*} [topological_space M₁] [add_comm_monoid M₁]
 {M₂ : Type*} [topological_space M₂] [add_comm_monoid M₂]
 {M₃ : Type*} [topological_space M₃] [add_comm_monoid M₃]
 {M₄ : Type*} [topological_space M₄] [add_comm_monoid M₄]
 [module R₁ M₁] [module R₂ M₂] [module R₃ M₃]
-{σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂]
-{σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [ring_hom_inv_pair σ₂₃ σ₃₂] [ring_hom_inv_pair σ₃₂ σ₂₃]
-{σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [ring_hom_inv_pair σ₁₃ σ₃₁] [ring_hom_inv_pair σ₃₁ σ₁₃]
-[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
 
 include σ₂₁
 /-- A continuous linear equivalence induces a continuous linear map. -/
@@ -1207,6 +1213,16 @@ by { ext, refl }
   e.to_homeomorph.symm = e.symm.to_homeomorph :=
 rfl
 
+/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
+  because it is a composition of multiple projections. -/
+def simps.apply (h : M₁ ≃SL[σ₁₂] M₂) : M₁ → M₂ := h
+
+/-- See Note [custom simps projection] -/
+def simps.symm_apply (h : M₁ ≃SL[σ₁₂] M₂) : M₂ → M₁ := h.symm
+
+initialize_simps_projections continuous_linear_equiv
+  (to_linear_equiv_to_fun → apply, to_linear_equiv_inv_fun → symm_apply)
+
 lemma symm_map_nhds_eq (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁) : map e.symm (𝓝 (e x)) = 𝓝 x :=
 e.to_homeomorph.symm_map_nhds_eq x
 omit σ₂₁
@@ -1316,6 +1332,13 @@ e.to_linear_equiv.to_equiv.image_eq_preimage s
 
 protected lemma image_symm_eq_preimage (e : M₁ ≃SL[σ₁₂] M₂) (s : set M₂) : e.symm '' s = e ⁻¹' s :=
 by rw [e.symm.image_eq_preimage, e.symm_symm]
+
+@[simp] protected lemma symm_preimage_preimage (e : M₁ ≃SL[σ₁₂] M₂) (s : set M₂) :
+  e.symm ⁻¹' (e ⁻¹' s) = s := e.to_linear_equiv.to_equiv.symm_preimage_preimage s
+
+@[simp] protected lemma preimage_symm_preimage (e : M₁ ≃SL[σ₁₂] M₂) (s : set M₁) :
+  e ⁻¹' (e.symm ⁻¹' s) = s := e.symm.symm_preimage_preimage s
+
 omit σ₂₁
 
 /-- Create a `continuous_linear_equiv` from two `continuous_linear_map`s that are
@@ -1528,6 +1551,20 @@ variables {ι R M}
 @[simp] lemma coe_fun_unique : ⇑(fun_unique ι R M) = function.eval (default ι) := rfl
 @[simp] lemma coe_fun_unique_symm : ⇑(fun_unique ι R M).symm = function.const ι := rfl
 
+variables (R M)
+
+/-- Continuous linear equivalence between dependent functions `Π i : fin 2, M i` and `M 0 × M 1`. -/
+@[simps { fully_applied := ff }]
+def pi_fin_two (M : fin 2 → Type*) [Π i, add_comm_monoid (M i)] [Π i, module R (M i)]
+  [Π i, topological_space (M i)] :
+  (Π i, M i) ≃L[R] M 0 × M 1 :=
+{ to_linear_equiv := linear_equiv.pi_fin_two R M, .. homeomorph.pi_fin_two M }
+
+/-- Continuous linear equivalence between vectors in `M² = fin 2 → M` and `M × M`. -/
+@[simps { fully_applied := ff }]
+def fin_two_arrow : (fin 2 → M) ≃L[R] M × M :=
+{ to_linear_equiv := linear_equiv.fin_two_arrow R M, .. pi_fin_two R (λ _, M) }
+
 end
 
 end continuous_linear_equiv

src/topology/homeomorph.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Patrick Massot, Sébastien Gouëzel, Zhouhang Zhou, Reid Barton
 -/
 import topology.dense_embedding
+import data.equiv.fin
 
 /-!
 # Homeomorphisms
@@ -399,6 +400,17 @@ def fun_unique (ι α : Type*) [unique ι] [topological_space α] : (ι → α)
   continuous_to_fun := continuous_apply _,
   continuous_inv_fun := continuous_pi (λ _, continuous_id) }
 
+/-- Homeomorphism between dependent functions `Π i : fin 2, α i` and `α 0 × α 1`. -/
+@[simps { fully_applied := ff }]
+def {u} pi_fin_two (α : fin 2 → Type u) [Π i, topological_space (α i)] : (Π i, α i) ≃ₜ α 0 × α 1 :=
+{ to_equiv := pi_fin_two_equiv α,
+  continuous_to_fun := (continuous_apply 0).prod_mk (continuous_apply 1),
+  continuous_inv_fun := continuous_pi $ fin.forall_fin_two.2 ⟨continuous_fst, continuous_snd⟩ }
+
+/-- Homeomorphism between `α² = fin 2 → α` and `α × α`. -/
+@[simps { fully_applied := ff }] def fin_two_arrow : (fin 2 → α) ≃ₜ α × α :=
+{ to_equiv := fin_two_arrow_equiv α, ..  pi_fin_two (λ _, α) }
+
 /--
 A subset of a topological space is homeomorphic to its image under a homeomorphism.
 -/