Pointwise instances on affine_subspaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file provides the additive action affine_subspace.pointwise_add_action in the
pointwise locale.
@[protected]
def
affine_subspace.pointwise_add_action
{k : Type u_1}
[ring k]
{V : Type u_2}
{P : Type u_3}
[add_comm_group V]
[module k V]
[add_torsor V P] :
add_action V (affine_subspace k P)
The additive action on an affine subspace corresponding to applying the action to every element.
This is available as an instance in the pointwise locale.
Equations
- affine_subspace.pointwise_add_action = {to_has_vadd := {vadd := λ (x : V) (S : affine_subspace k P), affine_subspace.map ↑(affine_equiv.const_vadd k P x) S}, zero_vadd := _, add_vadd := _}
@[simp]
theorem
affine_subspace.coe_pointwise_vadd
{k : Type u_1}
[ring k]
{V : Type u_2}
{P : Type u_3}
[add_comm_group V]
[module k V]
[add_torsor V P]
(v : V)
(s : affine_subspace k P) :
theorem
affine_subspace.vadd_mem_pointwise_vadd_iff
{k : Type u_1}
[ring k]
{V : Type u_2}
{P : Type u_3}
[add_comm_group V]
[module k V]
[add_torsor V P]
{v : V}
{s : affine_subspace k P}
{p : P} :
theorem
affine_subspace.pointwise_vadd_bot
{k : Type u_1}
[ring k]
{V : Type u_2}
{P : Type u_3}
[add_comm_group V]
[module k V]
[add_torsor V P]
(v : V) :
theorem
affine_subspace.pointwise_vadd_direction
{k : Type u_1}
[ring k]
{V : Type u_2}
{P : Type u_3}
[add_comm_group V]
[module k V]
[add_torsor V P]
(v : V)
(s : affine_subspace k P) :
theorem
affine_subspace.pointwise_vadd_span
{k : Type u_1}
[ring k]
{V : Type u_2}
{P : Type u_3}
[add_comm_group V]
[module k V]
[add_torsor V P]
(v : V)
(s : set P) :
v +ᵥ affine_span k s = affine_span k (v +ᵥ s)
theorem
affine_subspace.map_pointwise_vadd
{k : Type u_1}
[ring k]
{V₁ : Type u_4}
{P₁ : Type u_5}
{V₂ : Type u_6}
{P₂ : Type u_7}
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(f : P₁ →ᵃ[k] P₂)
(v : V₁)
(s : affine_subspace k P₁) :
affine_subspace.map f (v +ᵥ s) = ⇑(f.linear) v +ᵥ affine_subspace.map f s