feat(linear_algebra/affine_space/affine_map): add affine_map.proj (#…

…4850)

src/linear_algebra/affine_space/affine_map.lean

@@ -412,6 +412,30 @@ begin
   simp only [set.image_add_const_interval, set.image_mul_const_interval]
 end
 
+section
+
+variables {ι : Type*} {V : Π i : ι, Type*} {P : Π i : ι, Type*} [Π i, add_comm_group (V i)]
+  [Π i, semimodule k (V i)] [Π i, add_torsor (V i) (P i)]
+
+include V
+
+/-- Evaluation at a point as an affine map. -/
+def proj (i : ι) : (Π i : ι, P i) →ᵃ[k] P i :=
+{ to_fun := λ f, f i,
+  linear := @linear_map.proj k ι _ V _ _ i,
+  map_vadd' := λ p v, rfl }
+
+@[simp] lemma proj_apply (i : ι) (f : Π i, P i) : @proj k _ ι V P _ _ _ i f = f i := rfl
+
+@[simp] lemma proj_linear (i : ι) :
+   (@proj k _ ι V P _ _ _ i).linear = @linear_map.proj k ι _ V _ _ i := rfl
+
+lemma pi_line_map_apply (f g : Π i, P i) (c : k) (i : ι) :
+  line_map f g c i = line_map (f i) (g i) c :=
+(proj i : (Π i, P i) →ᵃ[k] P i).apply_line_map f g c
+
+end
+
 end affine_map
 
 namespace affine_map

src/linear_algebra/affine_space/midpoint.lean

@@ -133,6 +133,11 @@ lemma homothety_one_half {k : Type*} {V P : Type*} [field k] [char_zero k]
   homothety a (1/2:k) b = midpoint k a b :=
 by rw [one_div, homothety_inv_two]
 
+@[simp] lemma pi_midpoint_apply {k ι : Type*} {V : Π i : ι, Type*} {P : Π i : ι, Type*} [field k]
+  [invertible (2:k)] [Π i, add_comm_group (V i)] [Π i, semimodule k (V i)]
+  [Π i, add_torsor (V i) (P i)] (f g : Π i, P i) (i : ι) :
+  midpoint k f g i = midpoint k (f i) (g i) := rfl
+
 namespace add_monoid_hom
 
 variables (R R' : Type*) {E F : Type*}