feat(linear_algebra/pi): pi_option_equiv_prod (#9003)

Author: ChrisHughes24

src/data/equiv/basic.lean

@@ -794,6 +794,15 @@ def option_is_some_equiv (α : Type*) : {x : option α // x.is_some} ≃ α :=
   left_inv := λ o, subtype.eq $ option.some_get _,
   right_inv := λ x, option.get_some _ _ }
 
+/-- The product over `option α` of `β a` is the binary product of the
+product over `α` of `β (some α)` and `β none` -/
+@[simps] def pi_option_equiv_prod {α : Type*} {β : option α → Type*} :
+  (Π a : option α, β a) ≃ (β none × Π a : α, β (some a)) :=
+{ to_fun := λ f, (f none, λ a, f (some a)),
+  inv_fun := λ x a, option.cases_on a x.fst x.snd,
+  left_inv := λ f, funext $ λ a, by cases a; refl,
+  right_inv := λ x, by simp }
+
 /-- `α ⊕ β` is equivalent to a `sigma`-type over `bool`. Note that this definition assumes `α` and
 `β` to be types from the same universe, so it cannot by used directly to transfer theorems about
 sigma types to theorems about sum types. In many cases one can use `ulift` to work around this

src/linear_algebra/pi.lean

@@ -279,6 +279,14 @@ This is `equiv.Pi_congr_left` as a `linear_equiv` -/
 def Pi_congr_left (e : ι' ≃ ι) : (Π i', φ (e i')) ≃ₗ[R] (Π i, φ i) :=
 (Pi_congr_left' R φ e.symm).symm
 
+/-- This is `equiv.pi_option_equiv_prod` as a `linear_equiv` -/
+def pi_option_equiv_prod {ι : Type*} {M : option ι → Type*}
+  [Π i, add_comm_group (M i)] [Π i, module R (M i)] :
+  (Π i : option ι, M i) ≃ₗ[R] (M none × Π i : ι, M (some i)) :=
+{ map_add' := by simp [function.funext_iff],
+  map_smul' := by simp [function.funext_iff],
+  ..equiv.pi_option_equiv_prod }
+
 variables (ι R M) (S : Type*) [fintype ι] [decidable_eq ι] [semiring S]
   [add_comm_monoid M] [module R M] [module S M] [smul_comm_class R S M]