Pointwise instances on AffineSubspaces #
This file provides the additive action AffineSubspace.pointwiseAddAction in the
Pointwise locale.
def
AffineSubspace.pointwiseAddAction
{k : Type u_1}
[Ring k]
{V : Type u_2}
{P : Type u_3}
[AddCommGroup V]
[Module k V]
[AddTorsor V P]
:
AddAction V (AffineSubspace 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
- One or more equations did not get rendered due to their size.
Instances For
theorem
AffineSubspace.pointwise_vadd_eq_map
{k : Type u_1}
[Ring k]
{V : Type u_2}
{P : Type u_3}
[AddCommGroup V]
[Module k V]
[AddTorsor V P]
(v : V)
(s : AffineSubspace k P)
:
v +ᵥ s = AffineSubspace.map (↑(AffineEquiv.constVAdd k P v)) s
@[simp]
theorem
AffineSubspace.coe_pointwise_vadd
{k : Type u_1}
[Ring k]
{V : Type u_2}
{P : Type u_3}
[AddCommGroup V]
[Module k V]
[AddTorsor V P]
(v : V)
(s : AffineSubspace k P)
:
theorem
AffineSubspace.vadd_mem_pointwise_vadd_iff
{k : Type u_1}
[Ring k]
{V : Type u_2}
{P : Type u_3}
[AddCommGroup V]
[Module k V]
[AddTorsor V P]
{v : V}
{s : AffineSubspace k P}
{p : P}
:
theorem
AffineSubspace.pointwise_vadd_direction
{k : Type u_1}
[Ring k]
{V : Type u_2}
{P : Type u_3}
[AddCommGroup V]
[Module k V]
[AddTorsor V P]
(v : V)
(s : AffineSubspace k P)
:
theorem
AffineSubspace.pointwise_vadd_span
{k : Type u_1}
[Ring k]
{V : Type u_2}
{P : Type u_3}
[AddCommGroup V]
[Module k V]
[AddTorsor V P]
(v : V)
(s : Set P)
:
v +ᵥ affineSpan k s = affineSpan k (v +ᵥ s)
theorem
AffineSubspace.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}
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
[AddCommGroup V₂]
[Module k V₂]
[AddTorsor V₂ P₂]
(f : P₁ →ᵃ[k] P₂)
(v : V₁)
(s : AffineSubspace k P₁)
:
AffineSubspace.map f (v +ᵥ s) = f.linear v +ᵥ AffineSubspace.map f s