Documentation

Mathlib.LinearAlgebra.AffineSpace.Pointwise

Pointwise instances on AffineSubspaces #

This file provides the additive action AffineSubspace.pointwiseAddAction in the Pointwise locale.

source
def AffineSubspace.pointwiseVAdd {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] :
VAdd 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
source
@[simp]
theorem AffineSubspace.coe_pointwise_vadd {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (v : V) (s : AffineSubspace k P) :
↑(v +ᵥ s) = v +ᵥ ↑s
source
def AffineSubspace.pointwiseAddAction {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [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
source
theorem AffineSubspace.pointwise_vadd_eq_map {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (v : V) (s : AffineSubspace k P) :
v +ᵥ s = AffineSubspace.map (↑(AffineEquiv.constVAdd k P v)) s
source
theorem AffineSubspace.vadd_mem_pointwise_vadd_iff {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {v : V} {s : AffineSubspace k P} {p : P} :
v +ᵥ p ∈ v +ᵥ s ↔ p ∈ s
source
@[simp]
theorem AffineSubspace.pointwise_vadd_bot {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (v : V) :
v +ᵥ ⊥ = ⊥
source
@[simp]
theorem AffineSubspace.pointwise_vadd_top {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (v : V) :
v +ᵥ ⊤ = ⊤
source
theorem AffineSubspace.pointwise_vadd_direction {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (v : V) (s : AffineSubspace k P) :
(v +ᵥ s).direction = s.direction
source
theorem AffineSubspace.pointwise_vadd_span {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (v : V) (s : Set P) :
v +ᵥ affineSpan k s = affineSpan k (v +ᵥ s)
source
theorem AffineSubspace.map_pointwise_vadd {k : Type u_2} {V₁ : Type u_5} {P₁ : Type u_6} {V₂ : Type u_7} {P₂ : Type u_8} [Ring k] [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
source
def AffineSubspace.pointwiseSMul {M : Type u_1} {k : Type u_2} {V : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [Monoid M] [DistribMulAction M V] [SMulCommClass M k V] :
SMul M (AffineSubspace k V)

The multiplicative action on an affine subspace corresponding to applying the action to every element.

This is available as an instance in the Pointwise locale.

TODO: generalize to include SMul (P ≃ᵃ[k] P) (AffineSubspace k P), which acts on P with a VAdd version of a DistribMulAction.

Equations
source
@[simp]
theorem AffineSubspace.coe_smul {M : Type u_1} {k : Type u_2} {V : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [Monoid M] [DistribMulAction M V] [SMulCommClass M k V] (a : M) (s : AffineSubspace k V) :
↑(a • s) = a • ↑s
source
def AffineSubspace.mulAction {M : Type u_1} {k : Type u_2} {V : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [Monoid M] [DistribMulAction M V] [SMulCommClass M k V] :
MulAction M (AffineSubspace k V)

The multiplicative action on an affine subspace corresponding to applying the action to every element.

This is available as an instance in the Pointwise locale.

TODO: generalize to include SMul (P ≃ᵃ[k] P) (AffineSubspace k P), which acts on P with a VAdd version of a DistribMulAction.

Equations
source
theorem AffineSubspace.smul_eq_map {M : Type u_1} {k : Type u_2} {V : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [Monoid M] [DistribMulAction M V] [SMulCommClass M k V] (a : M) (s : AffineSubspace k V) :
a • s = AffineSubspace.map (DistribMulAction.toLinearMap k V a).toAffineMap s
source
theorem AffineSubspace.smul_mem_smul_iff {k : Type u_2} {V : Type u_3} [Ring k] [AddCommGroup V] [Module k V] {s : AffineSubspace k V} {p : V} {G : Type u_9} [Group G] [DistribMulAction G V] [SMulCommClass G k V] {a : G} :
a • p ∈ a • s ↔ p ∈ s
source
theorem AffineSubspace.smul_mem_smul_iff_of_isUnit {M : Type u_1} {k : Type u_2} {V : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [Monoid M] [DistribMulAction M V] [SMulCommClass M k V] {a : M} {s : AffineSubspace k V} {p : V} (ha : IsUnit a) :
a • p ∈ a • s ↔ p ∈ s
source
theorem AffineSubspace.smul_mem_smul_iff₀ {k : Type u_2} {V : Type u_3} [Ring k] [AddCommGroup V] [Module k V] {s : AffineSubspace k V} {p : V} {G₀ : Type u_9} [GroupWithZero G₀] [DistribMulAction G₀ V] [SMulCommClass G₀ k V] {a : G₀} (ha : a ≠ 0) :
a • p ∈ a • s ↔ p ∈ s
source
@[simp]
theorem AffineSubspace.smul_bot {M : Type u_1} {k : Type u_2} {V : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [Monoid M] [DistribMulAction M V] [SMulCommClass M k V] (a : M) :
a • ⊥ = ⊥
source
@[simp]
theorem AffineSubspace.smul_top {M : Type u_1} {k : Type u_2} {V : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [Monoid M] [DistribMulAction M V] [SMulCommClass M k V] {a : M} (ha : IsUnit a) :
a • ⊤ = ⊤
source
theorem AffineSubspace.smul_span {M : Type u_1} {k : Type u_2} {V : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [Monoid M] [DistribMulAction M V] [SMulCommClass M k V] (a : M) (s : Set V) :
a • affineSpan k s = affineSpan k (a • s)
source
@[simp]
theorem AffineSubspace.direction_smul {k : Type u_2} {V : Type u_3} [Field k] [AddCommGroup V] [Module k V] {a : k} (ha : a ≠ 0) (s : AffineSubspace k V) :
(a • s).direction = s.direction