Mathlib.LinearAlgebra.AffineSpace.Pointwise

AffineSubspace.pointwiseVAdd definition

: VAdd V (AffineSubspace k P)

Full source

/-- 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. -/
protected def pointwiseVAdd : VAdd V (AffineSubspace k P) where
  vadd x s := s.map (AffineEquiv.constVAdd k P x)

Vector addition action on affine subspaces

Informal description

The additive action of a vector space $V$ on the set of affine subspaces of an affine space $P$ over $V$ is defined by translating each point in the affine subspace by a fixed vector $x \in V$. More precisely, for any vector $x \in V$ and any affine subspace $s \subseteq P$, the action $x +ᵥ s$ is the image of $s$ under the affine automorphism of $P$ given by translation by $x$.

AffineSubspace.coe_pointwise_vadd theorem

(v : V) (s : AffineSubspace k P) : ((v +ᵥ s : AffineSubspace k P) : Set P) = v +ᵥ (s : Set P)

Full source

@[simp, norm_cast] lemma coe_pointwise_vadd (v : V) (s : AffineSubspace k P) :
    ((v +ᵥ s : AffineSubspace k P) : Set P) = v +ᵥ (s : Set P) := rfl

Translation of Affine Subspace Underlying Set by Vector

Informal description

For any vector $v \in V$ and any affine subspace $s$ of an affine space $P$ over $V$, the underlying set of the translated affine subspace $v +ᵥ s$ is equal to the translation of the underlying set of $s$ by $v$. That is, $(v +ᵥ s) = v +ᵥ s$ as sets.

AffineSubspace.pointwiseAddAction definition

: AddAction V (AffineSubspace k P)

Full source

/-- 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. -/
protected def pointwiseAddAction : AddAction V (AffineSubspace k P) :=
  SetLike.coe_injective.addAction _ coe_pointwise_vadd

Additive action on affine subspaces by vector translation

Informal description

The additive action of a vector space $V$ on the set of affine subspaces of an affine space $P$ over $V$ is defined by translating each point in the affine subspace by a fixed vector $v \in V$. More precisely, for any vector $v \in V$ and any affine subspace $s \subseteq P$, the action $v +ᵥ s$ is the image of $s$ under the affine automorphism of $P$ given by translation by $v$. This action satisfies the properties of an additive action, meaning that $0 +ᵥ s = s$ and $(v + w) +ᵥ s = v +ᵥ (w +ᵥ s)$ for all $v, w \in V$ and $s \subseteq P$.

AffineSubspace.pointwise_vadd_eq_map theorem

(v : V) (s : AffineSubspace k P) : v +ᵥ s = s.map (AffineEquiv.constVAdd k P v)

Full source

theorem pointwise_vadd_eq_map (v : V) (s : AffineSubspace k P) :
    v +ᵥ s = s.map (AffineEquiv.constVAdd k P v) :=
  rfl

Translation of Affine Subspace as Image under Translation Map

Informal description

For any vector $v$ in the vector space $V$ associated to an affine space $P$ over a ring $k$, and any affine subspace $s$ of $P$, the translation of $s$ by $v$ (denoted $v +ᵥ s$) is equal to the image of $s$ under the affine automorphism of $P$ given by translation by $v$.

AffineSubspace.vadd_mem_pointwise_vadd_iff theorem

{v : V} {s : AffineSubspace k P} {p : P} : v +ᵥ p ∈ v +ᵥ s ↔ p ∈ s

Full source

theorem vadd_mem_pointwise_vadd_iff {v : V} {s : AffineSubspace k P} {p : P} :
    v +ᵥ pv +ᵥ p ∈ v +ᵥ sv +ᵥ p ∈ v +ᵥ s ↔ p ∈ s :=
  vadd_mem_vadd_set_iff

Translation Invariance of Membership in Affine Subspaces

Informal description

For any vector $v \in V$, any affine subspace $s \subseteq P$, and any point $p \in P$, the translated point $v + p$ belongs to the translated affine subspace $v + s$ if and only if $p$ belongs to $s$.

AffineSubspace.pointwise_vadd_bot theorem

(v : V) : v +ᵥ (⊥ : AffineSubspace k P) = ⊥

Full source

@[simp] theorem pointwise_vadd_bot (v : V) : v +ᵥ (⊥ : AffineSubspace k P) = ⊥ := by
  ext; simp [pointwise_vadd_eq_map, map_bot]

Translation of Empty Affine Subspace is Empty

Informal description

For any vector $v$ in the vector space $V$ associated with an affine space $P$ over a ring $k$, the translation of the empty affine subspace (denoted $\bot$) by $v$ is equal to the empty affine subspace. In other words, $v +ᵥ \bot = \bot$.

AffineSubspace.pointwise_vadd_top theorem

(v : V) : v +ᵥ (⊤ : AffineSubspace k P) = ⊤

Full source

@[simp] lemma pointwise_vadd_top (v : V) : v +ᵥ (⊤ : AffineSubspace k P) = ⊤ := by
  ext; simp [pointwise_vadd_eq_map, map_top, vadd_eq_iff_eq_neg_vadd]

Translation of Entire Affine Space by a Vector Preserves the Space

Informal description

For any vector $v$ in the vector space $V$ associated with an affine space $P$ over a ring $k$, the translation of the entire affine space $P$ (represented as the top element $\top$ in the lattice of affine subspaces) by $v$ is equal to $P$ itself. In other words, $v +ᵥ P = P$.

AffineSubspace.pointwise_vadd_direction theorem

(v : V) (s : AffineSubspace k P) : (v +ᵥ s).direction = s.direction

Full source

theorem pointwise_vadd_direction (v : V) (s : AffineSubspace k P) :
    (v +ᵥ s).direction = s.direction := by
  rw [pointwise_vadd_eq_map, map_direction]
  exact Submodule.map_id _

Invariance of Direction under Translation of Affine Subspace

Informal description

For any vector $v$ in the vector space $V$ associated with an affine space $P$ over a ring $k$, and any affine subspace $s$ of $P$, the direction of the translated subspace $v +ᵥ s$ is equal to the direction of $s$. In symbols: $$ \text{direction}(v +ᵥ s) = \text{direction}(s). $$

AffineSubspace.pointwise_vadd_span theorem

(v : V) (s : Set P) : v +ᵥ affineSpan k s = affineSpan k (v +ᵥ s)

Full source

theorem pointwise_vadd_span (v : V) (s : Set P) : v +ᵥ affineSpan k s = affineSpan k (v +ᵥ s) :=
  map_span _ s

Affine Span Commutes with Translation

Informal description

For any vector $v$ in the vector space $V$ associated with an affine space $P$ over a ring $k$, and any subset $s$ of $P$, the translation of the affine span of $s$ by $v$ is equal to the affine span of the translation of $s$ by $v$. In symbols: $$ v +ᵥ \text{affineSpan}_k s = \text{affineSpan}_k (v +ᵥ s). $$

AffineSubspace.map_pointwise_vadd theorem

(f : P₁ →ᵃ[k] P₂) (v : V₁) (s : AffineSubspace k P₁) : (v +ᵥ s).map f = f.linear v +ᵥ s.map f

Full source

theorem map_pointwise_vadd (f : P₁ →ᵃ[k] P₂) (v : V₁) (s : AffineSubspace k P₁) :
    (v +ᵥ s).map f = f.linear v +ᵥ s.map f := by
  rw [pointwise_vadd_eq_map, pointwise_vadd_eq_map, map_map, map_map]
  congr 1
  ext
  exact f.map_vadd _ _

Compatibility of Affine Map with Translation and Subspace Image

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$ with associated vector spaces $V_1$ and $V_2$ respectively. Given an affine map $f \colon P_1 \to P_2$, a vector $v \in V_1$, and an affine subspace $s$ of $P_1$, the image under $f$ of the translation $v +ᵥ s$ is equal to the translation by $f.linear(v)$ of the image of $s$ under $f$. In symbols: $$ f(v +ᵥ s) = f.linear(v) +ᵥ f(s). $$

AffineSubspace.pointwiseSMul definition

: SMul M (AffineSubspace k V)

Full source

/-- 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`. -/
protected def pointwiseSMul : SMul M (AffineSubspace k V) where
  smul a s := s.map (DistribMulAction.toLinearMap k _ a).toAffineMap

Pointwise scalar multiplication on affine subspaces

Informal description

The scalar multiplication action on an affine subspace, where applying a scalar $a$ from a monoid $M$ to an affine subspace $s$ results in the image of $s$ under the affine map induced by the linear map corresponding to the scalar multiplication by $a$. More precisely, for a scalar $a \in M$ and an affine subspace $s$ of an affine space $V$ over a ring $k$, the action $a \bullet s$ is defined as the image of $s$ under the affine map associated with the linear map $v \mapsto a \bullet v$.

AffineSubspace.coe_smul theorem

(a : M) (s : AffineSubspace k V) : ↑(a • s) = a • (s : Set V)

Full source

@[simp, norm_cast]
lemma coe_smul (a : M) (s : AffineSubspace k V) : ↑(a • s) = a • (s : Set V) := rfl

Equality of Underlying Sets in Pointwise Scalar Multiplication of Affine Subspaces

Informal description

Let $k$ be a ring, $V$ be an additive commutative group with a $k$-module structure, and $P$ be an affine space over $V$. For any scalar $a$ in a monoid $M$ and any affine subspace $s$ of $V$, the underlying set of the scalar multiple $a \bullet s$ is equal to the pointwise scalar multiplication of $a$ on the underlying set of $s$, i.e., $$ \uparrow(a \bullet s) = a \bullet (\uparrow s) $$ where $\uparrow$ denotes the underlying set of an affine subspace.

AffineSubspace.mulAction definition

: MulAction M (AffineSubspace k V)

Full source

/-- 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`. -/
protected def mulAction : MulAction M (AffineSubspace k V) :=
  SetLike.coe_injective.mulAction _ coe_smul

Multiplicative action on affine subspaces

Informal description

The multiplicative action on an affine subspace, where for any scalar $a$ in a monoid $M$ and any affine subspace $s$ of an affine space $V$ over a ring $k$, the action $a \bullet s$ is defined as the image of $s$ under the affine map associated with the linear map $v \mapsto a \bullet v$. More precisely, this action satisfies: 1. $1 \bullet s = s$ for the identity element $1 \in M$ and any affine subspace $s$. 2. $(a \cdot b) \bullet s = a \bullet (b \bullet s)$ for any $a, b \in M$ and any affine subspace $s$.

AffineSubspace.smul_eq_map theorem

(a : M) (s : AffineSubspace k V) : a • s = s.map (DistribMulAction.toLinearMap k _ a).toAffineMap

Full source

lemma smul_eq_map (a : M) (s : AffineSubspace k V) :
    a • s = s.map (DistribMulAction.toLinearMap k _ a).toAffineMap := rfl

Pointwise Scalar Multiplication of Affine Subspace as Affine Map Image

Informal description

For any scalar $a$ in a monoid $M$ and any affine subspace $s$ of an affine space $V$ over a ring $k$, the pointwise scalar multiplication $a \bullet s$ is equal to the image of $s$ under the affine map induced by the linear map $v \mapsto a \bullet v$.

AffineSubspace.smul_mem_smul_iff theorem

{G : Type*} [Group G] [DistribMulAction G V] [SMulCommClass G k V] {a : G} : a • p ∈ a • s ↔ p ∈ s

Full source

lemma smul_mem_smul_iff {G : Type*} [Group G] [DistribMulAction G V] [SMulCommClass G k V] {a : G} :
    a • p ∈ a • sa • p ∈ a • s ↔ p ∈ s := smul_mem_smul_set_iff

Membership in Scaled Affine Subspace: $a \cdot p \in a \cdot s \leftrightarrow p \in s$

Informal description

Let $G$ be a group acting distributively on a vector space $V$ over a ring $k$, with the action commuting with the scalar multiplication by $k$. For any element $a \in G$, a point $p \in P$, and an affine subspace $s$ of $P$, the point $a \cdot p$ belongs to the scaled affine subspace $a \cdot s$ if and only if $p$ belongs to $s$.

AffineSubspace.smul_mem_smul_iff_of_isUnit theorem

(ha : IsUnit a) : a • p ∈ a • s ↔ p ∈ s

Full source

lemma smul_mem_smul_iff_of_isUnit (ha : IsUnit a) : a • p ∈ a • sa • p ∈ a • s ↔ p ∈ s :=
  smul_mem_smul_iff (a := ha.unit)

Membership in Scaled Affine Subspace for Units: $a \cdot p \in a \cdot s \leftrightarrow p \in s$ when $a$ is invertible

Informal description

Let $V$ be a vector space over a ring $k$, and let $P$ be an affine space over $V$. For any element $a$ in a monoid $M$ that acts distributively on $V$ with the action commuting with the scalar multiplication by $k$, if $a$ is a unit (i.e., invertible), then for any point $p \in P$ and any affine subspace $s$ of $P$, the point $a \cdot p$ belongs to the scaled affine subspace $a \cdot s$ if and only if $p$ belongs to $s$.

AffineSubspace.smul_mem_smul_iff₀ theorem

 {G₀ : Type*} [GroupWithZero G₀] [DistribMulAction G₀ V] [SMulCommClass G₀ k V] {a : G₀} (ha : a ≠ 0) :
  a • p ∈ a • s ↔ p ∈ s

Full source

lemma smul_mem_smul_iff₀ {G₀ : Type*} [GroupWithZero G₀] [DistribMulAction G₀ V]
    [SMulCommClass G₀ k V] {a : G₀} (ha : a ≠ 0) : a • p ∈ a • sa • p ∈ a • s ↔ p ∈ s :=
  smul_mem_smul_iff_of_isUnit ha.isUnit

Membership in Scaled Affine Subspace for Nonzero Scalars: $a \cdot p \in a \cdot s \leftrightarrow p \in s$ when $a \neq 0$

Informal description

Let $G₀$ be a group with zero acting distributively on a vector space $V$ over a ring $k$, with the action commuting with the scalar multiplication by $k$. For any nonzero element $a \in G₀$, a point $p \in P$, and an affine subspace $s$ of $P$, the point $a \cdot p$ belongs to the scaled affine subspace $a \cdot s$ if and only if $p$ belongs to $s$.

AffineSubspace.smul_bot theorem

(a : M) : a • (⊥ : AffineSubspace k V) = ⊥

Full source

@[simp] lemma smul_bot (a : M) : a • (⊥ : AffineSubspace k V) = ⊥ := by
  ext; simp [smul_eq_map, map_bot]

Scalar Multiplication Preserves Empty Affine Subspace

Informal description

For any element $a$ in a monoid $M$ acting on an affine space $V$ over a ring $k$, the scalar multiplication of $a$ with the bottom affine subspace $\bot$ (the empty subspace) equals $\bot$ itself, i.e., $a \bullet \bot = \bot$.

AffineSubspace.smul_top theorem

(ha : IsUnit a) : a • (⊤ : AffineSubspace k V) = ⊤

Full source

@[simp] lemma smul_top (ha : IsUnit a) : a • (⊤ : AffineSubspace k V) = ⊤ := by
  ext x; simpa [smul_eq_map, map_top] using ⟨ha.unit⁻¹ • x, smul_inv_smul ha.unit _⟩

Scalar Multiplication Preserves Top Affine Subspace for Units

Informal description

For any unit element $a$ in a monoid $M$ acting on an affine space $V$ over a ring $k$, the scalar multiplication of $a$ with the top affine subspace $\top$ (the entire space $V$) equals $\top$ itself, i.e., $a \bullet \top = \top$.

AffineSubspace.smul_span theorem

(a : M) (s : Set V) : a • affineSpan k s = affineSpan k (a • s)

Full source

lemma smul_span (a : M) (s : Set V) : a • affineSpan k s = affineSpan k (a • s) := map_span _ s

Affine Span Commutes with Scalar Multiplication

Informal description

For any scalar $a$ in a monoid $M$ and any subset $s$ of an affine space $V$ over a ring $k$, the scalar multiplication of $a$ with the affine span of $s$ is equal to the affine span of the scalar multiplication of $a$ with $s$. In symbols: $$ a \bullet \text{affineSpan}_k s = \text{affineSpan}_k (a \bullet s). $$

AffineSubspace.direction_smul theorem

(ha : a ≠ 0) (s : AffineSubspace k V) : (a • s).direction = s.direction

Full source

@[simp]
lemma direction_smul (ha : a ≠ 0) (s : AffineSubspace k V) : (a • s).direction = s.direction := by
  have : DistribMulAction.toLinearMap k V a = a • LinearMap.id := by
    ext; simp
  simp [smul_eq_map, map_direction, this, Submodule.map_smul, ha]

Invariance of Direction under Nonzero Scalar Multiplication of Affine Subspaces

Informal description

Let $k$ be a ring, $V$ be an additive commutative group with a $k$-module structure, and $P$ be an affine space over $V$. For any nonzero scalar $a \in M$ and any affine subspace $s$ of $P$, the direction of the scaled affine subspace $a \bullet s$ is equal to the direction of $s$, i.e., \[ \text{direction}(a \bullet s) = \text{direction}(s). \]