Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

vectorSpan_vadd theorem

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

Full source

@[simp] lemma vectorSpan_vadd (s : Set P) (v : V) : vectorSpan k (v +ᵥ s) = vectorSpan k s := by
  simp [vectorSpan]

Invariance of Vector Span under Translation

Informal description

For any set $s$ of points in an affine space over a module $V$ and any vector $v \in V$, the vector span of the translated set $v + s$ is equal to the vector span of $s$. That is, $\text{vectorSpan}_k(v + s) = \text{vectorSpan}_k(s)$.

AffineSubspace.vsub_right_mem_direction_iff_mem theorem

{s : AffineSubspace k P} {p : P} (hp : p ∈ s) (p₂ : P) : p₂ -ᵥ p ∈ s.direction ↔ p₂ ∈ s

Full source

/-- Given a point in an affine subspace, a result of subtracting that point on the right is in the
direction if and only if the other point is in the subspace. -/
theorem vsub_right_mem_direction_iff_mem {s : AffineSubspace k P} {p : P} (hp : p ∈ s) (p₂ : P) :
    p₂ -ᵥ pp₂ -ᵥ p ∈ s.directionp₂ -ᵥ p ∈ s.direction ↔ p₂ ∈ s := by
  rw [mem_direction_iff_eq_vsub_right hp]
  simp

Characterization of Affine Subspace Membership via Right Subtraction

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be an affine subspace of $P$. For any point $p \in s$ and any point $p_2 \in P$, the vector $p_2 - p$ belongs to the direction of $s$ if and only if $p_2$ is in $s$.

AffineSubspace.vsub_left_mem_direction_iff_mem theorem

{s : AffineSubspace k P} {p : P} (hp : p ∈ s) (p₂ : P) : p -ᵥ p₂ ∈ s.direction ↔ p₂ ∈ s

Full source

/-- Given a point in an affine subspace, a result of subtracting that point on the left is in the
direction if and only if the other point is in the subspace. -/
theorem vsub_left_mem_direction_iff_mem {s : AffineSubspace k P} {p : P} (hp : p ∈ s) (p₂ : P) :
    p -ᵥ p₂p -ᵥ p₂ ∈ s.directionp -ᵥ p₂ ∈ s.direction ↔ p₂ ∈ s := by
  rw [mem_direction_iff_eq_vsub_left hp]
  simp

Characterization of Affine Subspace Membership via Left Subtraction

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be an affine subspace of $P$. For any point $p \in s$ and any point $p_2 \in P$, the vector $p - p_2$ belongs to the direction of $s$ if and only if $p_2$ is in $s$.

AffineSubspace.toAddTorsor abbrev

(s : AffineSubspace k P) [Nonempty s] : AddTorsor s.direction s

Full source

/-- This is not an instance because it loops with `AddTorsor.nonempty`. -/
abbrev toAddTorsor (s : AffineSubspace k P) [Nonempty s] : AddTorsor s.direction s where
  vadd a b := ⟨(a : V) +ᵥ (b : P), vadd_mem_of_mem_direction a.2 b.2⟩
  zero_vadd := fun a => by
    ext
    exact zero_vadd _ _
  add_vadd a b c := by
    ext
    apply add_vadd
  vsub a b := ⟨(a : P) -ᵥ (b : P), (vsub_left_mem_direction_iff_mem a.2 _).mpr b.2⟩
  vsub_vadd' a b := by
    ext
    apply AddTorsor.vsub_vadd'
  vadd_vsub' a b := by
    ext
    apply AddTorsor.vadd_vsub'

Nonempty Affine Subspace as Additive Torsor Over Its Direction

Informal description

For any nonempty affine subspace $s$ of an affine space $P$ over a module $V$ with scalar ring $k$, the subspace $s$ forms an additive torsor over its direction submodule $s.\text{direction} \subseteq V$.

AffineSubspace.coe_vsub theorem

(s : AffineSubspace k P) [Nonempty s] (a b : s) : ↑(a -ᵥ b) = (a : P) -ᵥ (b : P)

Full source

@[simp, norm_cast]
theorem coe_vsub (s : AffineSubspace k P) [Nonempty s] (a b : s) : ↑(a -ᵥ b) = (a : P) -ᵥ (b : P) :=
  rfl

Coercion of Vector Subtraction in Affine Subspace Equals Vector Subtraction in Ambient Space

Informal description

For any nonempty affine subspace $s$ of an affine space $P$ over a module $V$ with scalar ring $k$, and for any two points $a, b \in s$, the coercion of the vector subtraction $a -ᵥ b$ in $s$ equals the vector subtraction of the coercions of $a$ and $b$ in $P$, i.e., $(a -ᵥ b) = (a : P) -ᵥ (b : P)$.

AffineSubspace.coe_vadd theorem

(s : AffineSubspace k P) [Nonempty s] (a : s.direction) (b : s) : ↑(a +ᵥ b) = (a : V) +ᵥ (b : P)

Full source

@[simp, norm_cast]
theorem coe_vadd (s : AffineSubspace k P) [Nonempty s] (a : s.direction) (b : s) :
    ↑(a +ᵥ b) = (a : V) +ᵥ (b : P) :=
  rfl

Coercion of Affine Combination in Nonempty Affine Subspace

Informal description

Let $s$ be a nonempty affine subspace of an affine space $P$ over a module $V$ with scalar ring $k$. For any vector $a$ in the direction of $s$ and any point $b$ in $s$, the coercion of the affine combination $a +ᵥ b$ in $s$ equals the affine combination $(a : V) +ᵥ (b : P)$ in $P$.

AffineSubspace.subtype definition

(s : AffineSubspace k P) [Nonempty s] : s →ᵃ[k] P

Full source

/-- Embedding of an affine subspace to the ambient space, as an affine map. -/
protected def subtype (s : AffineSubspace k P) [Nonempty s] : s →ᵃ[k] P where
  toFun := (↑)
  linear := s.direction.subtype
  map_vadd' _ _ := rfl

Embedding of an affine subspace into the ambient space

Informal description

For a nonempty affine subspace $ s $ of an affine space $ P $ over a module $ V $ with scalar ring $ k $, the embedding of $ s $ into $ P $ is an affine map. More precisely, this is the affine map whose underlying function is the canonical inclusion $ s \hookrightarrow P $, and whose linear part is the inclusion of the direction submodule $ s.\text{direction} $ into $ V $.

AffineSubspace.subtype_linear theorem

(s : AffineSubspace k P) [Nonempty s] : s.subtype.linear = s.direction.subtype

Full source

@[simp]
theorem subtype_linear (s : AffineSubspace k P) [Nonempty s] :
    s.subtype.linear = s.direction.subtype := rfl

Linear Part of Affine Subspace Embedding Equals Direction Submodule Inclusion

Informal description

For any nonempty affine subspace $s$ of an affine space $P$ over a module $V$ with scalar ring $k$, the linear part of the embedding map $s \hookrightarrow P$ is equal to the inclusion map of the direction submodule $s.\text{direction}$ into $V$.

AffineSubspace.subtype_apply theorem

{s : AffineSubspace k P} [Nonempty s] (p : s) : s.subtype p = p

Full source

@[simp]
theorem subtype_apply {s : AffineSubspace k P} [Nonempty s] (p : s) : s.subtype p = p :=
  rfl

Embedding of Affine Subspace Points Preserves Identity

Informal description

For any nonempty affine subspace $s$ of an affine space $P$ over a module $V$ with scalar ring $k$, and for any point $p$ in $s$, the embedding of $p$ into $P$ via the canonical inclusion map equals $p$ itself.

AffineSubspace.subtype_injective theorem

(s : AffineSubspace k P) [Nonempty s] : Function.Injective s.subtype

Full source

theorem subtype_injective (s : AffineSubspace k P) [Nonempty s] : Function.Injective s.subtype :=
  Subtype.coe_injective

Injectivity of the Affine Subspace Embedding

Informal description

For any nonempty affine subspace $s$ of an affine space $P$ over a module $V$ with scalar ring $k$, the canonical embedding $s \hookrightarrow P$ is injective. In other words, if two points in $s$ are equal when considered as points in $P$, then they are equal in $s$.

AffineSubspace.coe_subtype theorem

(s : AffineSubspace k P) [Nonempty s] : (s.subtype : s → P) = ((↑) : s → P)

Full source

@[simp]
theorem coe_subtype (s : AffineSubspace k P) [Nonempty s] : (s.subtype : s → P) = ((↑) : s → P) :=
  rfl

Embedding of Affine Subspace Coincides with Inclusion

Informal description

For any nonempty affine subspace $s$ of an affine space $P$ over a module $V$ with scalar ring $k$, the underlying function of the embedding $s \hookrightarrow P$ coincides with the canonical inclusion map from $s$ to $P$.

AffineMap.lineMap_mem theorem

 {k V P : Type*} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {Q : AffineSubspace k P} {p₀ p₁ : P} (c : k)
  (h₀ : p₀ ∈ Q) (h₁ : p₁ ∈ Q) : AffineMap.lineMap p₀ p₁ c ∈ Q

Full source

theorem AffineMap.lineMap_mem {k V P : Type*} [Ring k] [AddCommGroup V] [Module k V]
    [AddTorsor V P] {Q : AffineSubspace k P} {p₀ p₁ : P} (c : k) (h₀ : p₀ ∈ Q) (h₁ : p₁ ∈ Q) :
    AffineMap.lineMapAffineMap.lineMap p₀ p₁ c ∈ Q := by
  rw [AffineMap.lineMap_apply]
  exact Q.smul_vsub_vadd_mem c h₁ h₀ h₀

Affine Combinations Preserve Affine Subspace Membership

Informal description

Let $k$ be a ring, $V$ an additive commutative group with a $k$-module structure, and $P$ an affine space over $V$. Let $Q$ be an affine subspace of $P$. For any points $p_0, p_1 \in Q$ and any scalar $c \in k$, the affine combination $\text{lineMap}(p_0, p_1, c)$ lies in $Q$. Here, $\text{lineMap}(p_0, p_1, c)$ denotes the affine combination $(1 - c) \cdot p_0 + c \cdot p_1$ in the affine space $P$.

AffineSubspace.coe_affineSpan_singleton theorem

(p : P) : (affineSpan k ({ p } : Set P) : Set P) = { p }

Full source

/-- The affine span of a single point, coerced to a set, contains just that point. -/
@[simp 1001] -- Porting note: this needs to take priority over `coe_affineSpan`
theorem coe_affineSpan_singleton (p : P) : (affineSpan k ({p} : Set P) : Set P) = {p} := by
  ext x
  rw [mem_coe, ← vsub_right_mem_direction_iff_mem (mem_affineSpan k (Set.mem_singleton p)) _,
    direction_affineSpan]
  simp

Affine Span of Singleton Set is the Set Itself

Informal description

For any point $p$ in an affine space $P$ over a module $V$ with scalar ring $k$, the affine span of the singleton set $\{p\}$, when viewed as a subset of $P$, is equal to $\{p\}$ itself.

AffineSubspace.mem_affineSpan_singleton theorem

: p₁ ∈ affineSpan k ({ p₂ } : Set P) ↔ p₁ = p₂

Full source

/-- A point is in the affine span of a single point if and only if they are equal. -/
@[simp]
theorem mem_affineSpan_singleton : p₁ ∈ affineSpan k ({p₂} : Set P)p₁ ∈ affineSpan k ({p₂} : Set P) ↔ p₁ = p₂ := by
  simp [← mem_coe]

Characterization of Membership in Affine Span of a Singleton: $p_1 \in \text{affineSpan}(\{p_2\}) \leftrightarrow p_1 = p_2$

Informal description

For any two points $p_1$ and $p_2$ in an affine space $P$ over a module $V$ with scalar ring $k$, the point $p_1$ belongs to the affine span of the singleton set $\{p_2\}$ if and only if $p_1 = p_2$.

AffineSubspace.unique_affineSpan_singleton instance

(p : P) : Unique (affineSpan k { p })

Full source

instance unique_affineSpan_singleton (p : P) : Unique (affineSpan k {p}) where
  default := ⟨p, mem_affineSpan _ (Set.mem_singleton _)⟩
  uniq := fun x ↦ Subtype.ext ((mem_affineSpan_singleton _ _).1 x.property)

Uniqueness of the Affine Span of a Singleton Set

Informal description

For any point $p$ in an affine space $P$ over a module $V$ with scalar ring $k$, the affine span of the singleton set $\{p\}$ has a unique element.

AffineSubspace.preimage_coe_affineSpan_singleton theorem

(x : P) : ((↑) : affineSpan k ({ x } : Set P) → P) ⁻¹' { x } = univ

Full source

@[simp]
theorem preimage_coe_affineSpan_singleton (x : P) :
    ((↑) : affineSpan k ({x} : Set P) → P) ⁻¹' {x} = univ :=
  eq_univ_of_forall fun y => (AffineSubspace.mem_affineSpan_singleton _ _).1 y.2

Preimage of Singleton under Inclusion from Affine Span is Universal Set

Informal description

For any point $x$ in an affine space $P$ over a module $V$ with scalar ring $k$, the preimage of the singleton set $\{x\}$ under the canonical inclusion map from the affine span of $\{x\}$ to $P$ is the universal set (i.e., every point in the affine span of $\{x\}$ maps to $x$ under the inclusion).

AffineSubspace.topEquiv definition

: (⊤ : AffineSubspace k P) ≃ᵃ[k] P

Full source

/-- The top affine subspace is linearly equivalent to the affine space.
This is the affine version of `Submodule.topEquiv`. -/
@[simps! linear apply symm_apply_coe]
def topEquiv : (⊤ : AffineSubspace k P) ≃ᵃ[k] P where
  toEquiv := Equiv.Set.univ P
  linear := .ofEq.ofEq _ _ (direction_top _ _ _) ≪≫ₗ Submodule.topEquiv
  map_vadd' _ _ := rfl

Affine equivalence between the top affine subspace and the affine space

Informal description

The affine equivalence between the top affine subspace (the entire affine space $P$) and $P$ itself. More precisely, this equivalence consists of: 1. A bijection between the points of the top affine subspace and $P$, given by the identity map. 2. A linear equivalence between the direction of the top affine subspace (which is the entire module $V$) and $V$ itself, given by the identity map. 3. The property that this equivalence preserves the affine structure, meaning it respects the action of vectors on points.

AffineSubspace.subsingleton_of_subsingleton_span_eq_top theorem

{s : Set P} (h₁ : s.Subsingleton) (h₂ : affineSpan k s = ⊤) : Subsingleton P

Full source

theorem subsingleton_of_subsingleton_span_eq_top {s : Set P} (h₁ : s.Subsingleton)
    (h₂ : affineSpan k s = ⊤) : Subsingleton P := by
  obtain ⟨p, hp⟩ := AffineSubspace.nonempty_of_affineSpan_eq_top k V P h₂
  have : s = {p} := Subset.antisymm (fun q hq => h₁ hq hp) (by simp [hp])
  rw [this, AffineSubspace.ext_iff, AffineSubspace.coe_affineSpan_singleton,
    AffineSubspace.top_coe, eq_comm, ← subsingleton_iff_singleton (mem_univ _)] at h₂
  exact subsingleton_of_univ_subsingleton h₂

Affine Space is Subsingleton if Spanned by a Subsingleton Set

Informal description

For any set $s$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, if $s$ is a subsingleton (i.e., contains at most one point) and the affine span of $s$ equals the entire space $P$, then $P$ itself is a subsingleton (i.e., contains at most one point).

AffineSubspace.direction_lt_of_nonempty theorem

{s₁ s₂ : AffineSubspace k P} (h : s₁ < s₂) (hn : (s₁ : Set P).Nonempty) : s₁.direction < s₂.direction

Full source

/-- If one nonempty affine subspace is less than another, the same applies to their directions -/
theorem direction_lt_of_nonempty {s₁ s₂ : AffineSubspace k P} (h : s₁ < s₂)
    (hn : (s₁ : Set P).Nonempty) : s₁.direction < s₂.direction := by
  obtain ⟨p, hp⟩ := hn
  rw [lt_iff_le_and_exists] at h
  rcases h with ⟨hle, p₂, hp₂, hp₂s₁⟩
  rw [SetLike.lt_iff_le_and_exists]
  use direction_le hle, p₂ -ᵥ p, vsub_mem_direction hp₂ (hle hp)
  intro hm
  rw [vsub_right_mem_direction_iff_mem hp p₂] at hm
  exact hp₂s₁ hm

Strict Containment of Directions for Nonempty Affine Subspaces

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s_1$ and $s_2$ be affine subspaces of $P$ such that $s_1$ is strictly contained in $s_2$ (i.e., $s_1 \subset s_2$). If $s_1$ is nonempty, then the direction of $s_1$ is strictly contained in the direction of $s_2$ (i.e., $\text{direction}(s_1) \subset \text{direction}(s_2)$).

vectorSpan_eq_span_vsub_set_left theorem

{s : Set P} {p : P} (hp : p ∈ s) : vectorSpan k s = Submodule.span k ((p -ᵥ ·) '' s)

Full source

/-- The `vectorSpan` is the span of the pairwise subtractions with a given point on the left. -/
theorem vectorSpan_eq_span_vsub_set_left {s : Set P} {p : P} (hp : p ∈ s) :
    vectorSpan k s = Submodule.span k ((p -ᵥ ·) '' s) := by
  rw [vectorSpan_def]
  refine le_antisymm ?_ (Submodule.span_mono ?_)
  · rw [Submodule.span_le]
    rintro v ⟨p₁, hp₁, p₂, hp₂, hv⟩
    simp_rw [← vsub_sub_vsub_cancel_left p₁ p₂ p] at hv
    rw [← hv, SetLike.mem_coe, Submodule.mem_span]
    exact fun m hm => Submodule.sub_mem _ (hm ⟨p₂, hp₂, rfl⟩) (hm ⟨p₁, hp₁, rfl⟩)
  · rintro v ⟨p₂, hp₂, hv⟩
    exact ⟨p, hp, p₂, hp₂, hv⟩

Vector Span as Linear Span of Relative Vectors from a Fixed Point

Informal description

For a set $s$ of points in an affine space over a module $V$ and a point $p \in s$, the vector span of $s$ is equal to the linear span of the set of vectors obtained by subtracting $p$ from each point in $s$, i.e., $$\operatorname{vectorSpan}_k(s) = \operatorname{span}_k \{p - q \mid q \in s\}.$$

vectorSpan_eq_span_vsub_set_right theorem

{s : Set P} {p : P} (hp : p ∈ s) : vectorSpan k s = Submodule.span k ((· -ᵥ p) '' s)

Full source

/-- The `vectorSpan` is the span of the pairwise subtractions with a given point on the right. -/
theorem vectorSpan_eq_span_vsub_set_right {s : Set P} {p : P} (hp : p ∈ s) :
    vectorSpan k s = Submodule.span k ((· -ᵥ p) '' s) := by
  rw [vectorSpan_def]
  refine le_antisymm ?_ (Submodule.span_mono ?_)
  · rw [Submodule.span_le]
    rintro v ⟨p₁, hp₁, p₂, hp₂, hv⟩
    simp_rw [← vsub_sub_vsub_cancel_right p₁ p₂ p] at hv
    rw [← hv, SetLike.mem_coe, Submodule.mem_span]
    exact fun m hm => Submodule.sub_mem _ (hm ⟨p₁, hp₁, rfl⟩) (hm ⟨p₂, hp₂, rfl⟩)
  · rintro v ⟨p₂, hp₂, hv⟩
    exact ⟨p₂, hp₂, p, hp, hv⟩

Vector Span as Linear Span of Point Differences Relative to a Fixed Point

Informal description

For a set $s$ of points in an affine space over a module $V$ and a point $p \in s$, the vector span of $s$ is equal to the linear span of the set of vectors $\{q - p \mid q \in s\}$ in $V$.

vectorSpan_eq_span_vsub_set_left_ne theorem

{s : Set P} {p : P} (hp : p ∈ s) : vectorSpan k s = Submodule.span k ((p -ᵥ ·) '' (s \ { p }))

Full source

/-- The `vectorSpan` is the span of the pairwise subtractions with a given point on the left,
excluding the subtraction of that point from itself. -/
theorem vectorSpan_eq_span_vsub_set_left_ne {s : Set P} {p : P} (hp : p ∈ s) :
    vectorSpan k s = Submodule.span k ((p -ᵥ ·) '' (s \ {p})) := by
  conv_lhs =>
    rw [vectorSpan_eq_span_vsub_set_left k hp, ← Set.insert_eq_of_mem hp, ←
      Set.insert_diff_singleton, Set.image_insert_eq]
  simp [Submodule.span_insert_eq_span]

Vector Span as Linear Span of Relative Vectors from a Fixed Point (Excluding Itself)

Informal description

For a set $s$ of points in an affine space over a module $V$ and a point $p \in s$, the vector span of $s$ is equal to the linear span of the set of vectors obtained by subtracting $p$ from each point in $s \setminus \{p\}$, i.e., $$\operatorname{vectorSpan}_k(s) = \operatorname{span}_k \{p - q \mid q \in s \setminus \{p\}\}.$$

vectorSpan_eq_span_vsub_set_right_ne theorem

{s : Set P} {p : P} (hp : p ∈ s) : vectorSpan k s = Submodule.span k ((· -ᵥ p) '' (s \ { p }))

Full source

/-- The `vectorSpan` is the span of the pairwise subtractions with a given point on the right,
excluding the subtraction of that point from itself. -/
theorem vectorSpan_eq_span_vsub_set_right_ne {s : Set P} {p : P} (hp : p ∈ s) :
    vectorSpan k s = Submodule.span k ((· -ᵥ p) '' (s \ {p})) := by
  conv_lhs =>
    rw [vectorSpan_eq_span_vsub_set_right k hp, ← Set.insert_eq_of_mem hp, ←
      Set.insert_diff_singleton, Set.image_insert_eq]
  simp [Submodule.span_insert_eq_span]

Vector Span as Linear Span of Point Differences Relative to a Fixed Point (Excluding Self-Difference)

Informal description

For a set $s$ of points in an affine space over a module $V$ and a point $p \in s$, the vector span of $s$ is equal to the linear span of the set of vectors $\{q - p \mid q \in s \setminus \{p\}\}$ in $V$.

vectorSpan_eq_span_vsub_finset_right_ne theorem

 [DecidableEq P] [DecidableEq V] {s : Finset P} {p : P} (hp : p ∈ s) :
  vectorSpan k (s : Set P) = Submodule.span k ((s.erase p).image (· -ᵥ p))

Full source

/-- The `vectorSpan` is the span of the pairwise subtractions with a given point on the right,
excluding the subtraction of that point from itself. -/
theorem vectorSpan_eq_span_vsub_finset_right_ne [DecidableEq P] [DecidableEq V] {s : Finset P}
    {p : P} (hp : p ∈ s) :
    vectorSpan k (s : Set P) = Submodule.span k ((s.erase p).image (· -ᵥ p)) := by
  simp [vectorSpan_eq_span_vsub_set_right_ne _ (Finset.mem_coe.mpr hp)]

Vector Span of Finite Set as Linear Span of Relative Vectors from a Fixed Point

Informal description

For a finite set $s$ of points in an affine space over a module $V$ and a point $p \in s$, the vector span of $s$ is equal to the linear span of the set of vectors $\{q - p \mid q \in s \setminus \{p\}\}$ in $V$.

vectorSpan_image_eq_span_vsub_set_left_ne theorem

 (p : ι → P) {s : Set ι} {i : ι} (hi : i ∈ s) :
  vectorSpan k (p '' s) = Submodule.span k ((p i -ᵥ ·) '' (p '' (s \ { i })))

Full source

/-- The `vectorSpan` of the image of a function is the span of the pairwise subtractions with a
given point on the left, excluding the subtraction of that point from itself. -/
theorem vectorSpan_image_eq_span_vsub_set_left_ne (p : ι → P) {s : Set ι} {i : ι} (hi : i ∈ s) :
    vectorSpan k (p '' s) = Submodule.span k ((p i -ᵥ ·) '' (p '' (s \ {i}))) := by
  conv_lhs =>
    rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi, ←
      Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]
  simp [Submodule.span_insert_eq_span]

Vector Span of Image as Linear Span of Relative Vectors from a Fixed Point

Informal description

Let $p : \iota \to P$ be a function from an index set $\iota$ to points in an affine space $P$ over a module $V$, and let $s \subseteq \iota$ be a subset with $i \in s$. The vector span of the image $p(s)$ is equal to the linear span of the set of vectors obtained by subtracting $p(i)$ from each point in $p(s \setminus \{i\})$, i.e., $$ \operatorname{vectorSpan}_k(p(s)) = \operatorname{span}_k \{p(i) - p(j) \mid j \in s \setminus \{i\}\}. $$

vectorSpan_image_eq_span_vsub_set_right_ne theorem

 (p : ι → P) {s : Set ι} {i : ι} (hi : i ∈ s) :
  vectorSpan k (p '' s) = Submodule.span k ((· -ᵥ p i) '' (p '' (s \ { i })))

Full source

/-- The `vectorSpan` of the image of a function is the span of the pairwise subtractions with a
given point on the right, excluding the subtraction of that point from itself. -/
theorem vectorSpan_image_eq_span_vsub_set_right_ne (p : ι → P) {s : Set ι} {i : ι} (hi : i ∈ s) :
    vectorSpan k (p '' s) = Submodule.span k ((· -ᵥ p i) '' (p '' (s \ {i}))) := by
  conv_lhs =>
    rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi,
      ← Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]
  simp [Submodule.span_insert_eq_span]

Vector Span of Image as Linear Span of Point Differences Relative to a Fixed Point

Informal description

For a family of points $p : \iota \to P$ in an affine space over a module $V$, a set $s \subseteq \iota$, and an index $i \in s$, the vector span of the image $p(s)$ is equal to the linear span of the set of vectors $\{p(j) - p(i) \mid j \in s \setminus \{i\}\}$ in $V$.

vectorSpan_range_eq_span_range_vsub_left theorem

(p : ι → P) (i0 : ι) : vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i : ι => p i0 -ᵥ p i)

Full source

/-- The `vectorSpan` of an indexed family is the span of the pairwise subtractions with a given
point on the left. -/
theorem vectorSpan_range_eq_span_range_vsub_left (p : ι → P) (i0 : ι) :
    vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i : ι => p i0 -ᵥ p i) := by
  rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_range_self i0), ← Set.range_comp]
  congr

Vector Span of Point Range as Linear Span of Relative Vectors from a Fixed Point

Informal description

For an indexed family of points $p : \iota \to P$ in an affine space over a module $V$ and a fixed index $i_0 \in \iota$, the vector span of the range of $p$ is equal to the linear span of the range of the relative vectors from $p(i_0)$, i.e., $$\operatorname{vectorSpan}_k(\mathrm{range}(p)) = \operatorname{span}_k \{p(i_0) - p(i) \mid i \in \iota\}.$$

vectorSpan_range_eq_span_range_vsub_right theorem

(p : ι → P) (i0 : ι) : vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i : ι => p i -ᵥ p i0)

Full source

/-- The `vectorSpan` of an indexed family is the span of the pairwise subtractions with a given
point on the right. -/
theorem vectorSpan_range_eq_span_range_vsub_right (p : ι → P) (i0 : ι) :
    vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i : ι => p i -ᵥ p i0) := by
  rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_range_self i0), ← Set.range_comp]
  congr

Vector Span of Range Equals Linear Span of Point Differences Relative to a Fixed Index

Informal description

For any indexed family of points $p : \iota \to P$ in an affine space over a module $V$ and any index $i_0 \in \iota$, the vector span of the range of $p$ is equal to the linear span of the range of the vector differences $\{p(i) - p(i_0) \mid i \in \iota\}$ in $V$.

vectorSpan_range_eq_span_range_vsub_left_ne theorem

 (p : ι → P) (i₀ : ι) : vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i : { x // x ≠ i₀ } => p i₀ -ᵥ p i)

Full source

/-- The `vectorSpan` of an indexed family is the span of the pairwise subtractions with a given
point on the left, excluding the subtraction of that point from itself. -/
theorem vectorSpan_range_eq_span_range_vsub_left_ne (p : ι → P) (i₀ : ι) :
    vectorSpan k (Set.range p) =
      Submodule.span k (Set.range fun i : { x // x ≠ i₀ } => p i₀ -ᵥ p i) := by
  rw [← Set.image_univ, vectorSpan_image_eq_span_vsub_set_left_ne k _ (Set.mem_univ i₀)]
  congr with v
  simp only [Set.mem_range, Set.mem_image, Set.mem_diff, Set.mem_singleton_iff, Subtype.exists,
    Subtype.coe_mk]
  constructor
  · rintro ⟨x, ⟨i₁, ⟨⟨_, hi₁⟩, rfl⟩⟩, hv⟩
    exact ⟨i₁, hi₁, hv⟩
  · exact fun ⟨i₁, hi₁, hv⟩ => ⟨p i₁, ⟨i₁, ⟨Set.mem_univ _, hi₁⟩, rfl⟩, hv⟩

Vector Span of Range Equals Linear Span of Non-Identical Point Differences from Fixed Index

Informal description

For an indexed family of points $p : \iota \to P$ in an affine space over a module $V$ and a fixed index $i_0 \in \iota$, the vector span of the range of $p$ is equal to the linear span of the set of vectors $\{p(i_0) - p(i) \mid i \in \iota, i \neq i_0\}$ in $V$. That is, $$ \operatorname{vectorSpan}_k(\mathrm{range}(p)) = \operatorname{span}_k \{p(i_0) - p(i) \mid i \neq i_0\}. $$

vectorSpan_range_eq_span_range_vsub_right_ne theorem

 (p : ι → P) (i₀ : ι) : vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i : { x // x ≠ i₀ } => p i -ᵥ p i₀)

Full source

/-- The `vectorSpan` of an indexed family is the span of the pairwise subtractions with a given
point on the right, excluding the subtraction of that point from itself. -/
theorem vectorSpan_range_eq_span_range_vsub_right_ne (p : ι → P) (i₀ : ι) :
    vectorSpan k (Set.range p) =
      Submodule.span k (Set.range fun i : { x // x ≠ i₀ } => p i -ᵥ p i₀) := by
  rw [← Set.image_univ, vectorSpan_image_eq_span_vsub_set_right_ne k _ (Set.mem_univ i₀)]
  congr with v
  simp only [Set.mem_range, Set.mem_image, Set.mem_diff, Set.mem_singleton_iff, Subtype.exists,
    Subtype.coe_mk]
  constructor
  · rintro ⟨x, ⟨i₁, ⟨⟨_, hi₁⟩, rfl⟩⟩, hv⟩
    exact ⟨i₁, hi₁, hv⟩
  · exact fun ⟨i₁, hi₁, hv⟩ => ⟨p i₁, ⟨i₁, ⟨Set.mem_univ _, hi₁⟩, rfl⟩, hv⟩

Vector Span of Range as Linear Span of Non-Identical Point Differences Relative to a Fixed Index

Informal description

For any indexed family of points $p : \iota \to P$ in an affine space over a module $V$ and any index $i_0 \in \iota$, the vector span of the range of $p$ is equal to the linear span of the set of vectors $\{p(i) - p(i_0) \mid i \in \iota, i \neq i_0\}$ in $V$.

affineSpan_coe_preimage_eq_top theorem

(A : Set P) [Nonempty A] : affineSpan k (((↑) : affineSpan k A → P) ⁻¹' A) = ⊤

Full source

/-- A set, considered as a subset of its spanned affine subspace, spans the whole subspace. -/
@[simp]
theorem affineSpan_coe_preimage_eq_top (A : Set P) [Nonempty A] :
    affineSpan k (((↑) : affineSpan k A → P) ⁻¹' A) = ⊤ := by
  rw [eq_top_iff]
  rintro ⟨x, hx⟩ -
  refine affineSpan_induction' (fun y hy ↦ ?_) (fun c u hu v hv w hw ↦ ?_) hx
  · exact subset_affineSpan _ _ hy
  · exact AffineSubspace.smul_vsub_vadd_mem _ _

Affine Span of Preimage in its Own Span is the Whole Span

Informal description

For any nonempty subset $A$ of an affine space $P$ over a module $V$ with scalar ring $k$, the affine span of the preimage of $A$ under the canonical inclusion map from the affine span of $A$ to $P$ is equal to the entire affine span of $A$. In other words, if we consider $A$ as a subset of its own affine span, then the affine span of this subset is the whole affine span of $A$.

affineSpan_singleton_union_vadd_eq_top_of_span_eq_top theorem

 {s : Set V} (p : P) (h : Submodule.span k (Set.range ((↑) : s → V)) = ⊤) :
  affineSpan k ({ p } ∪ (fun v => v +ᵥ p) '' s) = ⊤

Full source

/-- Suppose a set of vectors spans `V`.  Then a point `p`, together with those vectors added to `p`,
spans `P`. -/
theorem affineSpan_singleton_union_vadd_eq_top_of_span_eq_top {s : Set V} (p : P)
    (h : Submodule.span k (Set.range ((↑) : s → V)) = ⊤) :
    affineSpan k ({p}{p} ∪ (fun v => v +ᵥ p) '' s) = ⊤ := by
  convert ext_of_direction_eq _
      ⟨p, mem_affineSpan k (Set.mem_union_left _ (Set.mem_singleton _)), mem_top k V p⟩
  rw [direction_affineSpan, direction_top,
    vectorSpan_eq_span_vsub_set_right k (Set.mem_union_left _ (Set.mem_singleton _) : p ∈ _),
    eq_top_iff, ← h]
  apply Submodule.span_mono
  rintro v ⟨v', rfl⟩
  use (v' : V) +ᵥ p
  simp

Affine Span of a Point and its Translations by a Spanning Set is the Entire Space

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be a subset of $V$ such that the linear span of $s$ is the entire module $V$ (i.e., $\operatorname{span}_k s = \top$). Then, for any point $p \in P$, the affine span of the union of the singleton set $\{p\}$ and the set of points obtained by translating $p$ by vectors in $s$ (i.e., $\{v + p \mid v \in s\}$) is the entire affine space $P$ (i.e., $\operatorname{affineSpan}_k (\{p\} \cup \{v + p \mid v \in s\}) = \top$).

vectorSpan_pair theorem

(p₁ p₂ : P) : vectorSpan k ({ p₁, p₂ } : Set P) = k ∙ p₁ -ᵥ p₂

Full source

/-- The `vectorSpan` of two points is the span of their difference. -/
theorem vectorSpan_pair (p₁ p₂ : P) : vectorSpan k ({p₁, p₂} : Set P) = k ∙ p₁ -ᵥ p₂ := by
  simp_rw [vectorSpan_eq_span_vsub_set_left k (mem_insert p₁ _), image_pair, vsub_self,
    Submodule.span_insert_zero]

Vector Span of Two Points is the Line Through Their Difference

Informal description

For any two points $p_1$ and $p_2$ in an affine space over a module $V$ with scalar field $k$, the vector span of the set $\{p_1, p_2\}$ is equal to the one-dimensional submodule generated by the vector difference $p_1 - p_2$, i.e., $$\operatorname{vectorSpan}_k(\{p_1, p_2\}) = k \cdot (p_1 - p_2).$$

vectorSpan_pair_rev theorem

(p₁ p₂ : P) : vectorSpan k ({ p₁, p₂ } : Set P) = k ∙ p₂ -ᵥ p₁

Full source

/-- The `vectorSpan` of two points is the span of their difference (reversed). -/
theorem vectorSpan_pair_rev (p₁ p₂ : P) : vectorSpan k ({p₁, p₂} : Set P) = k ∙ p₂ -ᵥ p₁ := by
  rw [pair_comm, vectorSpan_pair]

Vector Span of Two Points is the Line Through Their Reverse Difference

Informal description

For any two points $p_1$ and $p_2$ in an affine space over a module $V$ with scalar field $k$, the vector span of the set $\{p_1, p_2\}$ is equal to the one-dimensional submodule generated by the vector difference $p_2 - p_1$, i.e., $$\operatorname{vectorSpan}_k(\{p_1, p_2\}) = k \cdot (p_2 - p_1).$$

mem_vectorSpan_pair theorem

{p₁ p₂ : P} {v : V} : v ∈ vectorSpan k ({ p₁, p₂ } : Set P) ↔ ∃ r : k, r • (p₁ -ᵥ p₂) = v

Full source

/-- A vector lies in the `vectorSpan` of two points if and only if it is a multiple of their
difference. -/
theorem mem_vectorSpan_pair {p₁ p₂ : P} {v : V} :
    v ∈ vectorSpan k ({p₁, p₂} : Set P)v ∈ vectorSpan k ({p₁, p₂} : Set P) ↔ ∃ r : k, r • (p₁ -ᵥ p₂) = v := by
  rw [vectorSpan_pair, Submodule.mem_span_singleton]

Characterization of vectors in the span of two points: $v \in \operatorname{vectorSpan}_k(\{p_1, p_2\}) \leftrightarrow \exists r \in k, v = r \cdot (p_1 - p_2)$

Informal description

For any two points $p_1, p_2$ in an affine space over a module $V$ with scalar field $k$, a vector $v \in V$ lies in the vector span of $\{p_1, p_2\}$ if and only if there exists a scalar $r \in k$ such that $v = r \cdot (p_1 - p_2)$.

mem_vectorSpan_pair_rev theorem

{p₁ p₂ : P} {v : V} : v ∈ vectorSpan k ({ p₁, p₂ } : Set P) ↔ ∃ r : k, r • (p₂ -ᵥ p₁) = v

Full source

/-- A vector lies in the `vectorSpan` of two points if and only if it is a multiple of their
difference (reversed). -/
theorem mem_vectorSpan_pair_rev {p₁ p₂ : P} {v : V} :
    v ∈ vectorSpan k ({p₁, p₂} : Set P)v ∈ vectorSpan k ({p₁, p₂} : Set P) ↔ ∃ r : k, r • (p₂ -ᵥ p₁) = v := by
  rw [vectorSpan_pair_rev, Submodule.mem_span_singleton]

Characterization of vectors in the span of two points (reversed difference): $v \in \operatorname{vectorSpan}_k(\{p_1, p_2\}) \leftrightarrow \exists r \in k, v = r \cdot (p_2 - p_1)$

Informal description

For any two points $p_1, p_2$ in an affine space over a module $V$ with scalar field $k$, a vector $v \in V$ lies in the vector span of $\{p_1, p_2\}$ if and only if there exists a scalar $r \in k$ such that $v = r \cdot (p_2 - p_1)$.

AffineMap.lineMap_mem_affineSpan_pair theorem

(r : k) (p₁ p₂ : P) : AffineMap.lineMap p₁ p₂ r ∈ line[k, p₁, p₂]

Full source

/-- A combination of two points expressed with `lineMap` lies in their affine span. -/
theorem AffineMap.lineMap_mem_affineSpan_pair (r : k) (p₁ p₂ : P) :
    AffineMap.lineMapAffineMap.lineMap p₁ p₂ r ∈ line[k, p₁, p₂] :=
  AffineMap.lineMap_mem _ (left_mem_affineSpan_pair _ _ _) (right_mem_affineSpan_pair _ _ _)

Affine Combination of Two Points Lies in Their Affine Span

Informal description

For any scalar $r$ in the ring $k$ and any two points $p_1, p_2$ in an affine space $P$ over a module $V$ with scalar ring $k$, the affine combination $\text{lineMap}(p_1, p_2, r)$ lies in the affine span of the pair $\{p_1, p_2\}$. Here, $\text{lineMap}(p_1, p_2, r)$ denotes the affine combination $(1 - r) \cdot p_1 + r \cdot p_2$ in the affine space $P$, and $\text{affineSpan}_k \{p_1, p_2\}$ is the smallest affine subspace containing both $p_1$ and $p_2$.

AffineMap.lineMap_rev_mem_affineSpan_pair theorem

(r : k) (p₁ p₂ : P) : AffineMap.lineMap p₂ p₁ r ∈ line[k, p₁, p₂]

Full source

/-- A combination of two points expressed with `lineMap` (with the two points reversed) lies in
their affine span. -/
theorem AffineMap.lineMap_rev_mem_affineSpan_pair (r : k) (p₁ p₂ : P) :
    AffineMap.lineMapAffineMap.lineMap p₂ p₁ r ∈ line[k, p₁, p₂] :=
  AffineMap.lineMap_mem _ (right_mem_affineSpan_pair _ _ _) (left_mem_affineSpan_pair _ _ _)

Reversed Affine Combination in Affine Span of Pair

Informal description

For any scalar $r$ in a ring $k$ and any two points $p_1, p_2$ in an affine space $P$ over a module $V$ with scalar ring $k$, the affine combination $\text{lineMap}(p_2, p_1, r)$ lies in the affine span of the pair $\{p_1, p_2\}$. Here, $\text{lineMap}(p_2, p_1, r)$ denotes the affine combination $(1 - r) \cdot p_2 + r \cdot p_1$ in the affine space $P$, and $\text{affineSpan}_k \{p_1, p_2\}$ is the smallest affine subspace containing both $p_1$ and $p_2$.

smul_vsub_vadd_mem_affineSpan_pair theorem

(r : k) (p₁ p₂ : P) : r • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ line[k, p₁, p₂]

Full source

/-- A multiple of the difference of two points added to the first point lies in their affine
span. -/
theorem smul_vsub_vadd_mem_affineSpan_pair (r : k) (p₁ p₂ : P) :
    r • (p₂ -ᵥ p₁) +ᵥ p₁r • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ line[k, p₁, p₂] :=
  AffineMap.lineMap_mem_affineSpan_pair _ _ _

Scaled Difference Added to Point Lies in Affine Span of Pair

Informal description

For any scalar $r$ in the ring $k$ and any two points $p_1, p_2$ in an affine space $P$ over a module $V$ with scalar ring $k$, the point obtained by adding the vector $r \cdot (p_2 - p_1)$ to $p_1$ lies in the affine span of $\{p_1, p_2\}$. Here, $p_2 - p_1$ denotes the vector difference (vsub) between $p_2$ and $p_1$, and $r \cdot (p_2 - p_1) + p_1$ represents the vector addition (vadd) of the scaled difference to $p_1$.

smul_vsub_rev_vadd_mem_affineSpan_pair theorem

(r : k) (p₁ p₂ : P) : r • (p₁ -ᵥ p₂) +ᵥ p₂ ∈ line[k, p₁, p₂]

Full source

/-- A multiple of the difference of two points added to the second point lies in their affine
span. -/
theorem smul_vsub_rev_vadd_mem_affineSpan_pair (r : k) (p₁ p₂ : P) :
    r • (p₁ -ᵥ p₂) +ᵥ p₂r • (p₁ -ᵥ p₂) +ᵥ p₂ ∈ line[k, p₁, p₂] :=
  AffineMap.lineMap_rev_mem_affineSpan_pair _ _ _

Scaled Reverse Difference Lies in Affine Span of Two Points

Informal description

For any scalar $r$ in a ring $k$ and any two points $p_1, p_2$ in an affine space $P$ over a module $V$ with scalar ring $k$, the point $r \cdot (p_1 - p_2) + p_2$ lies in the affine span of the pair $\{p_1, p_2\}$. Here, $p_1 - p_2$ denotes the vector difference between $p_1$ and $p_2$ in the associated vector space $V$, and $+$ denotes the action of $V$ on $P$.

vadd_left_mem_affineSpan_pair theorem

{p₁ p₂ : P} {v : V} : v +ᵥ p₁ ∈ line[k, p₁, p₂] ↔ ∃ r : k, r • (p₂ -ᵥ p₁) = v

Full source

/-- A vector added to the first point lies in the affine span of two points if and only if it is
a multiple of their difference. -/
theorem vadd_left_mem_affineSpan_pair {p₁ p₂ : P} {v : V} :
    v +ᵥ p₁v +ᵥ p₁ ∈ line[k, p₁, p₂]v +ᵥ p₁ ∈ line[k, p₁, p₂] ↔ ∃ r : k, r • (p₂ -ᵥ p₁) = v := by
  rw [vadd_mem_iff_mem_direction _ (left_mem_affineSpan_pair _ _ _), direction_affineSpan,
    mem_vectorSpan_pair_rev]

Characterization of Affine Span Membership via Scaled Difference: $v + p_1 \in \text{affineSpan}_k\{p_1, p_2\} \leftrightarrow \exists r \in k, v = r \cdot (p_2 - p_1)$

Informal description

For any two points $p_1, p_2$ in an affine space $P$ over a module $V$ with scalar ring $k$, and for any vector $v \in V$, the point $v + p_1$ lies in the affine span of $\{p_1, p_2\}$ if and only if there exists a scalar $r \in k$ such that $v = r \cdot (p_2 - p_1)$.

vadd_right_mem_affineSpan_pair theorem

{p₁ p₂ : P} {v : V} : v +ᵥ p₂ ∈ line[k, p₁, p₂] ↔ ∃ r : k, r • (p₁ -ᵥ p₂) = v

Full source

/-- A vector added to the second point lies in the affine span of two points if and only if it is
a multiple of their difference. -/
theorem vadd_right_mem_affineSpan_pair {p₁ p₂ : P} {v : V} :
    v +ᵥ p₂v +ᵥ p₂ ∈ line[k, p₁, p₂]v +ᵥ p₂ ∈ line[k, p₁, p₂] ↔ ∃ r : k, r • (p₁ -ᵥ p₂) = v := by
  rw [vadd_mem_iff_mem_direction _ (right_mem_affineSpan_pair _ _ _), direction_affineSpan,
    mem_vectorSpan_pair]

Characterization of Points in Affine Span via Right Translation: $v + p_2 \in \operatorname{affineSpan}\{p_1, p_2\} \leftrightarrow \exists r \in k, v = r \cdot (p_1 - p_2)$

Informal description

For any two points $p_1, p_2$ in an affine space $P$ over a module $V$ with scalar ring $k$, and any vector $v \in V$, the point $v + p_2$ lies in the affine span of $\{p_1, p_2\}$ if and only if there exists a scalar $r \in k$ such that $v = r \cdot (p_1 - p_2)$.

AffineSubspace.direction_sup theorem

 {s₁ s₂ : AffineSubspace k P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s₁) (hp₂ : p₂ ∈ s₂) :
  (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction ⊔ k ∙ p₂ -ᵥ p₁

Full source

/-- The direction of the sup of two nonempty affine subspaces is the sup of the two directions and
of any one difference between points in the two subspaces. -/
theorem direction_sup {s₁ s₂ : AffineSubspace k P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s₁) (hp₂ : p₂ ∈ s₂) :
    (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.directions₁.direction ⊔ s₂.direction ⊔ k ∙ p₂ -ᵥ p₁ := by
  refine le_antisymm ?_ ?_
  · change (affineSpan k ((s₁ : Set P) ∪ s₂)).direction ≤ _
    rw [← mem_coe] at hp₁
    rw [direction_affineSpan, vectorSpan_eq_span_vsub_set_right k (Set.mem_union_left _ hp₁),
      Submodule.span_le]
    rintro v ⟨p₃, hp₃, rfl⟩
    rcases hp₃ with hp₃ | hp₃
    · rw [sup_assoc, sup_comm, SetLike.mem_coe, Submodule.mem_sup]
      use 0, Submodule.zero_mem _, p₃ -ᵥ p₁, vsub_mem_direction hp₃ hp₁
      rw [zero_add]
    · rw [sup_assoc, SetLike.mem_coe, Submodule.mem_sup]
      use 0, Submodule.zero_mem _, p₃ -ᵥ p₁
      rw [and_comm, zero_add]
      use rfl
      rw [← vsub_add_vsub_cancel p₃ p₂ p₁, Submodule.mem_sup]
      use p₃ -ᵥ p₂, vsub_mem_direction hp₃ hp₂, p₂ -ᵥ p₁, Submodule.mem_span_singleton_self _
  · refine sup_le (sup_direction_le _ _) ?_
    rw [direction_eq_vectorSpan, vectorSpan_def]
    exact
      sInf_le_sInf fun p hp =>
        Set.Subset.trans
          (Set.singleton_subset_iff.2
            (vsub_mem_vsub (mem_affineSpan k (Set.mem_union_right _ hp₂))
              (mem_affineSpan k (Set.mem_union_left _ hp₁))))
          hp

Direction of Supremum of Two Affine Subspaces as Supremum of Directions and Point Difference Span

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s_1$ and $s_2$ be two nonempty affine subspaces of $P$. For any points $p_1 \in s_1$ and $p_2 \in s_2$, the direction of the affine span $s_1 \sqcup s_2$ is equal to the supremum of the directions of $s_1$ and $s_2$ and the line spanned by the vector $p_2 - p_1$. That is, $$ \text{direction}(s_1 \sqcup s_2) = \text{direction}(s_1) \sqcup \text{direction}(s_2) \sqcup k \cdot (p_2 - p_1). $$

AffineSubspace.direction_sup_eq_sup_direction theorem

 {s₁ s₂ : AffineSubspace k P} {p : P} (hp₁ : p ∈ s₁) (hp₂ : p ∈ s₂) : (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction

Full source

/-- The direction of the sup of two affine subspaces with a common point is the sup of the two
directions. -/
lemma direction_sup_eq_sup_direction {s₁ s₂ : AffineSubspace k P} {p : P} (hp₁ : p ∈ s₁)
    (hp₂ : p ∈ s₂) : (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction := by
  rw [direction_sup hp₁ hp₂]
  simp

Direction of Supremum of Two Affine Subspaces with Common Point Equals Supremum of Directions

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s_1$ and $s_2$ be two affine subspaces of $P$ that share a common point $p \in s_1 \cap s_2$. Then the direction of the affine span $s_1 \sqcup s_2$ is equal to the supremum of the directions of $s_1$ and $s_2$, i.e., $$ \text{direction}(s_1 \sqcup s_2) = \text{direction}(s_1) \sqcup \text{direction}(s_2). $$

AffineSubspace.direction_affineSpan_insert theorem

 {s : AffineSubspace k P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) :
  (affineSpan k (insert p₂ (s : Set P))).direction = Submodule.span k {p₂ -ᵥ p₁} ⊔ s.direction

Full source

/-- The direction of the span of the result of adding a point to a nonempty affine subspace is the
sup of the direction of that subspace and of any one difference between that point and a point in
the subspace. -/
theorem direction_affineSpan_insert {s : AffineSubspace k P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) :
    (affineSpan k (insert p₂ (s : Set P))).direction =
    Submodule.spanSubmodule.span k {p₂ -ᵥ p₁} ⊔ s.direction := by
  rw [sup_comm, ← Set.union_singleton, ← coe_affineSpan_singleton k V p₂]
  change (s ⊔ affineSpan k {p₂}).direction = _
  rw [direction_sup hp₁ (mem_affineSpan k (Set.mem_singleton _)), direction_affineSpan]
  simp

Direction of Affine Span After Insertion Equals Supremum of Original Direction and Point Difference Span

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be a nonempty affine subspace of $P$. For any points $p_1 \in s$ and $p_2 \in P$, the direction of the affine span of $s \cup \{p_2\}$ is equal to the supremum of the direction of $s$ and the line spanned by the vector $p_2 - p_1$. That is, $$ \text{direction}(\text{affineSpan}_k(s \cup \{p_2\})) = \text{span}_k\{p_2 - p_1\} \sqcup \text{direction}(s). $$

AffineSubspace.mem_affineSpan_insert_iff theorem

 {s : AffineSubspace k P} {p₁ : P} (hp₁ : p₁ ∈ s) (p₂ p : P) :
  p ∈ affineSpan k (insert p₂ (s : Set P)) ↔ ∃ r : k, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁ : V) +ᵥ p0

Full source

/-- Given a point `p₁` in an affine subspace `s`, and a point `p₂`, a point `p` is in the span of
`s` with `p₂` added if and only if it is a multiple of `p₂ -ᵥ p₁` added to a point in `s`. -/
theorem mem_affineSpan_insert_iff {s : AffineSubspace k P} {p₁ : P} (hp₁ : p₁ ∈ s) (p₂ p : P) :
    p ∈ affineSpan k (insert p₂ (s : Set P))p ∈ affineSpan k (insert p₂ (s : Set P)) ↔
      ∃ r : k, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁ : V) +ᵥ p0 := by
  rw [← mem_coe] at hp₁
  rw [← vsub_right_mem_direction_iff_mem (mem_affineSpan k (Set.mem_insert_of_mem _ hp₁)),
    direction_affineSpan_insert hp₁, Submodule.mem_sup]
  constructor
  · rintro ⟨v₁, hv₁, v₂, hv₂, hp⟩
    rw [Submodule.mem_span_singleton] at hv₁
    rcases hv₁ with ⟨r, rfl⟩
    use r, v₂ +ᵥ p₁, vadd_mem_of_mem_direction hv₂ hp₁
    symm at hp
    rw [← sub_eq_zero, ← vsub_vadd_eq_vsub_sub, vsub_eq_zero_iff_eq] at hp
    rw [hp, vadd_vadd]
  · rintro ⟨r, p₃, hp₃, rfl⟩
    use r • (p₂ -ᵥ p₁), Submodule.mem_span_singleton.2 ⟨r, rfl⟩, p₃ -ᵥ p₁,
      vsub_mem_direction hp₃ hp₁
    rw [vadd_vsub_assoc]

Characterization of Affine Span Membership After Insertion via Scalar Multiple and Base Point

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be an affine subspace of $P$. Given a point $p_1 \in s$ and any points $p_2, p \in P$, the point $p$ lies in the affine span of $s \cup \{p_2\}$ if and only if there exists a scalar $r \in k$ and a point $p_0 \in s$ such that $p = r \cdot (p_2 - p_1) + p_0$.

AffineSubspace.vectorSpan_union_of_mem_of_mem theorem

 {s₁ s₂ : Set P} {p : P} (hp₁ : p ∈ s₁) (hp₂ : p ∈ s₂) : vectorSpan k (s₁ ∪ s₂) = vectorSpan k s₁ ⊔ vectorSpan k s₂

Full source

/-- The vector span of a union of sets with a common point is the sup of their vector spans. -/
lemma vectorSpan_union_of_mem_of_mem {s₁ s₂ : Set P} {p : P} (hp₁ : p ∈ s₁) (hp₂ : p ∈ s₂) :
    vectorSpan k (s₁ ∪ s₂) = vectorSpanvectorSpan k s₁ ⊔ vectorSpan k s₂ := by
  simp_rw [← direction_affineSpan, span_union,
    direction_sup_eq_sup_direction (mem_affineSpan k hp₁) (mem_affineSpan k hp₂)]

Vector Span of Union with Common Point Equals Supremum of Vector Spans

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s_1$ and $s_2$ be subsets of $P$ that share a common point $p \in s_1 \cap s_2$. Then the vector span of the union $s_1 \cup s_2$ is equal to the supremum of the vector spans of $s_1$ and $s_2$, i.e., $$ \text{vectorSpan}_k(s_1 \cup s_2) = \text{vectorSpan}_k(s_1) \sqcup \text{vectorSpan}_k(s_2). $$

AffineMap.vectorSpan_image_eq_submodule_map theorem

{s : Set P₁} : Submodule.map f.linear (vectorSpan k s) = vectorSpan k (f '' s)

Full source

@[simp]
theorem AffineMap.vectorSpan_image_eq_submodule_map {s : Set P₁} :
    Submodule.map f.linear (vectorSpan k s) = vectorSpan k (f '' s) := by
  simp [vectorSpan_def, f.image_vsub_image]

Vector Span Commutes with Affine Map Images

Informal description

For any affine map $f \colon P_1 \to P_2$ between affine spaces over a ring $k$, and any subset $s \subseteq P_1$, the vector span of the image $f(s)$ in $P_2$ is equal to the image under the linear part of $f$ of the vector span of $s$ in $P_1$. In symbols: \[ \operatorname{vectorSpan}_k (f(s)) = f_{\text{linear}}(\operatorname{vectorSpan}_k s). \]

AffineSubspace.map definition

(s : AffineSubspace k P₁) : AffineSubspace k P₂

Full source

/-- The image of an affine subspace under an affine map as an affine subspace. -/
def map (s : AffineSubspace k P₁) : AffineSubspace k P₂ where
  carrier := f '' s
  smul_vsub_vadd_mem := by
    rintro t - - - ⟨p₁, h₁, rfl⟩ ⟨p₂, h₂, rfl⟩ ⟨p₃, h₃, rfl⟩
    use t • (p₁ -ᵥ p₂) +ᵥ p₃
    suffices t • (p₁ -ᵥ p₂) +ᵥ p₃t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s by
    { simp only [SetLike.mem_coe, true_and, this]
      rw [AffineMap.map_vadd, map_smul, AffineMap.linearMap_vsub] }
    exact s.smul_vsub_vadd_mem t h₁ h₂ h₃

Image of an affine subspace under an affine map

Informal description

Given an affine map $f : P_1 \to P_2$ between affine spaces over a ring $k$, and an affine subspace $s$ of $P_1$, the image of $s$ under $f$ is an affine subspace of $P_2$. More precisely, the image consists of all points $f(p)$ where $p$ is in $s$, and it inherits the affine subspace structure from $s$ via the map $f$.

AffineSubspace.coe_map theorem

(s : AffineSubspace k P₁) : (s.map f : Set P₂) = f '' s

Full source

@[simp]
theorem coe_map (s : AffineSubspace k P₁) : (s.map f : Set P₂) = f '' s :=
  rfl

Image of Affine Subspace Under Affine Map Equals Set Image

Informal description

For any affine subspace $s$ of an affine space $P_1$ over a ring $k$, and any affine map $f : P_1 \to P_2$, the underlying set of the image of $s$ under $f$ is equal to the image of $s$ under $f$ as a set, i.e., $\text{map}(f)(s) = f(s)$.

AffineSubspace.mem_map theorem

{f : P₁ →ᵃ[k] P₂} {x : P₂} {s : AffineSubspace k P₁} : x ∈ s.map f ↔ ∃ y ∈ s, f y = x

Full source

@[simp]
theorem mem_map {f : P₁ →ᵃ[k] P₂} {x : P₂} {s : AffineSubspace k P₁} :
    x ∈ s.map fx ∈ s.map f ↔ ∃ y ∈ s, f y = x :=
  Iff.rfl

Characterization of Points in the Image of an Affine Subspace under an Affine Map

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$, and let $f : P_1 \to P_2$ be an affine map. For any affine subspace $s$ of $P_1$ and any point $x \in P_2$, we have $x \in \text{map}(f, s)$ if and only if there exists a point $y \in s$ such that $f(y) = x$.

AffineSubspace.mem_map_of_mem theorem

{x : P₁} {s : AffineSubspace k P₁} (h : x ∈ s) : f x ∈ s.map f

Full source

theorem mem_map_of_mem {x : P₁} {s : AffineSubspace k P₁} (h : x ∈ s) : f x ∈ s.map f :=
  Set.mem_image_of_mem _ h

Image of Point in Affine Subspace under Affine Map

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$, and let $f : P_1 \to P_2$ be an affine map. For any point $x \in P_1$ and any affine subspace $s \subseteq P_1$, if $x \in s$, then the image $f(x)$ belongs to the image of $s$ under $f$, denoted $s.map f$.

AffineSubspace.mem_map_iff_mem_of_injective theorem

 {f : P₁ →ᵃ[k] P₂} {x : P₁} {s : AffineSubspace k P₁} (hf : Function.Injective f) : f x ∈ s.map f ↔ x ∈ s

Full source

@[simp 1100, nolint simpNF]
theorem mem_map_iff_mem_of_injective {f : P₁ →ᵃ[k] P₂} {x : P₁} {s : AffineSubspace k P₁}
    (hf : Function.Injective f) : f x ∈ s.map ff x ∈ s.map f ↔ x ∈ s :=
  hf.mem_set_image

Injective Affine Map Preserves Affine Subspace Membership

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$, and let $f \colon P_1 \to P_2$ be an injective affine map. For any point $x \in P_1$ and any affine subspace $s \subseteq P_1$, the image $f(x)$ belongs to the image of $s$ under $f$ if and only if $x$ belongs to $s$. In symbols: \[ f(x) \in f(s) \leftrightarrow x \in s. \]

AffineSubspace.map_bot theorem

: (⊥ : AffineSubspace k P₁).map f = ⊥

Full source

@[simp]
theorem map_bot : (⊥ : AffineSubspace k P₁).map f = ⊥ :=
  coe_injective <| image_empty f

Image of Empty Affine Subspace is Empty

Informal description

The image of the bottom affine subspace (the empty subspace) under any affine map $f \colon P_1 \to P_2$ is the bottom affine subspace (the empty subspace) in $P_2$. In symbols: \[ f(\bot) = \bot. \]

AffineSubspace.map_eq_bot_iff theorem

{s : AffineSubspace k P₁} : s.map f = ⊥ ↔ s = ⊥

Full source

@[simp]
theorem map_eq_bot_iff {s : AffineSubspace k P₁} : s.map f = ⊥ ↔ s = ⊥ := by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rwa [← coe_eq_bot_iff, coe_map, image_eq_empty, coe_eq_bot_iff] at h
  · rw [h, map_bot]

Image of Affine Subspace is Empty iff Subspace is Empty

Informal description

For any affine subspace $s$ of an affine space $P_1$ over a ring $k$, the image of $s$ under an affine map $f \colon P_1 \to P_2$ is the empty affine subspace if and only if $s$ itself is the empty affine subspace. In symbols: $$ f(s) = \bot \leftrightarrow s = \bot. $$

AffineSubspace.map_id theorem

(s : AffineSubspace k P₁) : s.map (AffineMap.id k P₁) = s

Full source

@[simp]
theorem map_id (s : AffineSubspace k P₁) : s.map (AffineMap.id k P₁) = s :=
  coe_injective <| image_id _

Identity Affine Map Preserves Affine Subspace

Informal description

For any affine subspace $s$ of an affine space $P_1$ over a ring $k$, the image of $s$ under the identity affine map $\mathrm{id} : P_1 \to P_1$ is equal to $s$ itself, i.e., $\mathrm{id}(s) = s$.

AffineSubspace.map_map theorem

(s : AffineSubspace k P₁) (f : P₁ →ᵃ[k] P₂) (g : P₂ →ᵃ[k] P₃) : (s.map f).map g = s.map (g.comp f)

Full source

theorem map_map (s : AffineSubspace k P₁) (f : P₁ →ᵃ[k] P₂) (g : P₂ →ᵃ[k] P₃) :
    (s.map f).map g = s.map (g.comp f) :=
  coe_injective <| image_image _ _ _

Composition of Affine Maps Preserves Affine Subspace Image

Informal description

Let $s$ be an affine subspace of an affine space $P_1$ over a ring $k$, and let $f \colon P_1 \to P_2$ and $g \colon P_2 \to P_3$ be affine maps. Then the image of $s$ under $g \circ f$ is equal to the image under $g$ of the image of $s$ under $f$. In symbols: $$g(f(s)) = (g \circ f)(s).$$

AffineSubspace.map_direction theorem

(s : AffineSubspace k P₁) : (s.map f).direction = s.direction.map f.linear

Full source

@[simp]
theorem map_direction (s : AffineSubspace k P₁) :
    (s.map f).direction = s.direction.map f.linear := by
  simp [direction_eq_vectorSpan, AffineMap.vectorSpan_image_eq_submodule_map]

Direction of Affine Subspace Image under Affine Map

Informal description

Let $k$ be a ring, $V$ and $V'$ be modules over $k$, and $P_1$ and $P_2$ be affine spaces over $V$ and $V'$ respectively. Given an affine map $f \colon P_1 \to P_2$ with linear part $f_{\text{linear}} \colon V \to V'$, and an affine subspace $s$ of $P_1$, the direction of the image $f(s)$ is equal to the image under $f_{\text{linear}}$ of the direction of $s$. In symbols: \[ \text{direction}(f(s)) = f_{\text{linear}}(\text{direction}(s)). \]

AffineSubspace.map_span theorem

(s : Set P₁) : (affineSpan k s).map f = affineSpan k (f '' s)

Full source

theorem map_span (s : Set P₁) : (affineSpan k s).map f = affineSpan k (f '' s) := by
  rcases s.eq_empty_or_nonempty with (rfl | ⟨p, hp⟩)
  · simp
  apply ext_of_direction_eq
  · simp [direction_affineSpan]
  · exact ⟨f p, mem_image_of_mem f (subset_affineSpan k _ hp),
          subset_affineSpan k _ (mem_image_of_mem f hp)⟩

Affine Span Commutes with Affine Map Images

Informal description

For any set $s$ of points in an affine space $P_1$ over a module $V$ with scalar ring $k$, and any affine map $f \colon P_1 \to P_2$, the image under $f$ of the affine span of $s$ is equal to the affine span of the image $f(s)$. In symbols: $$ f(\text{affineSpan}_k s) = \text{affineSpan}_k (f(s)). $$

AffineSubspace.inclusion definition

(h : S₁ ≤ S₂) : S₁ →ᵃ[k] S₂

Full source

/-- Affine map from a smaller to a larger subspace of the same space.

This is the affine version of `Submodule.inclusion`. -/
@[simps linear]
def inclusion (h : S₁ ≤ S₂) : S₁ →ᵃ[k] S₂ where
  toFun := Set.inclusion h
  linear := Submodule.inclusion <| AffineSubspace.direction_le h
  map_vadd' := fun ⟨_,_⟩ ⟨_,_⟩ => rfl

Inclusion of affine subspaces

Informal description

Given two affine subspaces $ S_1 $ and $ S_2 $ of an affine space $ P $ over a module $ V $ with scalar ring $ k $, and an inclusion $ h : S_1 \leq S_2 $, the affine map $ \text{inclusion}(h) : S_1 \to S_2 $ is the canonical injection that maps each point of $ S_1 $ to itself, viewed as a point of $ S_2 $. This map is affine, meaning it preserves the affine structure, and its linear part is the inclusion of the direction submodule of $ S_1 $ into the direction submodule of $ S_2 $.

AffineSubspace.coe_inclusion_apply theorem

(h : S₁ ≤ S₂) (x : S₁) : (inclusion h x : P₁) = x

Full source

@[simp]
theorem coe_inclusion_apply (h : S₁ ≤ S₂) (x : S₁) : (inclusion h x : P₁) = x :=
  rfl

Inclusion Map Acts as Identity on Points of Affine Subspace

Informal description

For any two affine subspaces $ S_1 $ and $ S_2 $ of an affine space $ P $ over a module $ V $ with scalar ring $ k $, if $ S_1 $ is contained in $ S_2 $ (denoted by $ h : S_1 \leq S_2 $), then for any point $ x \in S_1 $, the image of $ x $ under the inclusion map $ \text{inclusion}(h) $ is equal to $ x $ itself when viewed as a point in $ P $. In other words, the inclusion map acts as the identity on points of $ S_1 $.

AffineSubspace.inclusion_rfl theorem

: inclusion (le_refl S₁) = AffineMap.id k S₁

Full source

@[simp]
theorem inclusion_rfl : inclusion (le_refl S₁) = AffineMap.id k S₁ := rfl

Inclusion of Affine Subspace into Itself is the Identity Map

Informal description

The inclusion map of an affine subspace $S_1$ into itself (via the reflexive order relation $S_1 \leq S_1$) is equal to the identity affine map on $S_1$.

AffineMap.map_top_of_surjective theorem

(hf : Function.Surjective f) : AffineSubspace.map f ⊤ = ⊤

Full source

@[simp]
theorem map_top_of_surjective (hf : Function.Surjective f) : AffineSubspace.map f ⊤ = ⊤ := by
  rw [AffineSubspace.ext_iff]
  exact image_univ_of_surjective hf

Surjective Affine Maps Preserve the Entire Space

Informal description

Let $f : P_1 \to P_2$ be a surjective affine map between affine spaces over a ring $k$. Then the image of the entire affine space $P_1$ (denoted by $\top$) under $f$ is equal to the entire affine space $P_2$ (also denoted by $\top$), i.e., $f(P_1) = P_2$.

AffineMap.span_eq_top_of_surjective theorem

{s : Set P₁} (hf : Function.Surjective f) (h : affineSpan k s = ⊤) : affineSpan k (f '' s) = ⊤

Full source

theorem span_eq_top_of_surjective {s : Set P₁} (hf : Function.Surjective f)
    (h : affineSpan k s = ⊤) : affineSpan k (f '' s) = ⊤ := by
  rw [← AffineSubspace.map_span, h, map_top_of_surjective f hf]

Surjective Affine Maps Preserve Spanning Sets

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$, $f \colon P_1 \to P_2$ a surjective affine map, and $s \subseteq P_1$ a set of points. If the affine span of $s$ equals the entire space $P_1$ (i.e., $\text{affineSpan}_k s = P_1$), then the affine span of the image $f(s)$ equals the entire space $P_2$ (i.e., $\text{affineSpan}_k (f(s)) = P_2$).

AffineEquiv.ofEq definition

(h : S₁ = S₂) : S₁ ≃ᵃ[k] S₂

Full source

/-- Affine equivalence between two equal affine subspace.

This is the affine version of `LinearEquiv.ofEq`. -/
@[simps linear]
def ofEq (h : S₁ = S₂) : S₁ ≃ᵃ[k] S₂ where
  toEquiv := Equiv.setCongr <| congr_arg _ h
  linear := .ofEq _ _ <| congr_arg _ h
  map_vadd' := fun ⟨_,_⟩ ⟨_,_⟩ => rfl

Affine equivalence between equal affine subspaces

Informal description

Given two affine subspaces $ S_1 $ and $ S_2 $ of an affine space $ P $ over a module $ V $ with scalar ring $ k $, and an equality $ h : S_1 = S_2 $, the affine equivalence $ S_1 \simeqᵃ[k] S_2 $ is defined. This equivalence maps each point in $ S_1 $ to the corresponding point in $ S_2 $ via the identity map, and its linear part is the identity linear map on the direction submodule.

AffineEquiv.coe_ofEq_apply theorem

(h : S₁ = S₂) (x : S₁) : (ofEq S₁ S₂ h x : P₁) = x

Full source

@[simp]
theorem coe_ofEq_apply (h : S₁ = S₂) (x : S₁) : (ofEq S₁ S₂ h x : P₁) = x :=
  rfl

Identity Preservation in Affine Equivalence of Equal Subspaces

Informal description

Given two affine subspaces $ S_1 $ and $ S_2 $ of an affine space $ P $ over a module $ V $ with scalar ring $ k $, and an equality $ h : S_1 = S_2 $, the affine equivalence $ \text{ofEq} \, S_1 \, S_2 \, h $ maps any point $ x \in S_1 $ to the corresponding point in $ S_2 $ such that the underlying point in $ P $ remains unchanged, i.e., $ \text{ofEq} \, S_1 \, S_2 \, h \, x = x $ as elements of $ P $.

AffineEquiv.ofEq_symm theorem

(h : S₁ = S₂) : (ofEq S₁ S₂ h).symm = ofEq S₂ S₁ h.symm

Full source

@[simp]
theorem ofEq_symm (h : S₁ = S₂) : (ofEq S₁ S₂ h).symm = ofEq S₂ S₁ h.symm := by
  ext
  rfl

Symmetry of Affine Equivalence Between Equal Subspaces

Informal description

Given two affine subspaces $ S_1 $ and $ S_2 $ of an affine space $ P $ over a module $ V $ with scalar ring $ k $, and an equality $ h : S_1 = S_2 $, the inverse of the affine equivalence $ \text{ofEq}~S_1~S_2~h $ is equal to the affine equivalence $ \text{ofEq}~S_2~S_1~h^{-1} $, where $ h^{-1} $ denotes the symmetry of the equality $ h $.

AffineEquiv.ofEq_rfl theorem

: ofEq S₁ S₁ rfl = AffineEquiv.refl k S₁

Full source

@[simp]
theorem ofEq_rfl : ofEq S₁ S₁ rfl = AffineEquiv.refl k S₁ := rfl

Identity Affine Equivalence via Reflexivity

Informal description

The affine equivalence between an affine subspace $S_1$ and itself (via reflexivity) is equal to the identity affine equivalence on $S_1$ over the ring $k$.

AffineEquiv.span_eq_top_iff theorem

{s : Set P₁} (e : P₁ ≃ᵃ[k] P₂) : affineSpan k s = ⊤ ↔ affineSpan k (e '' s) = ⊤

Full source

theorem span_eq_top_iff {s : Set P₁} (e : P₁ ≃ᵃ[k] P₂) :
    affineSpanaffineSpan k s = ⊤ ↔ affineSpan k (e '' s) = ⊤ := by
  refine ⟨(e : P₁ →ᵃ[k] P₂).span_eq_top_of_surjective e.surjective, ?_⟩
  intro h
  have : s = e.symm '' (e '' s) := by rw [← image_comp]; simp
  rw [this]
  exact (e.symm : P₂ →ᵃ[k] P₁).span_eq_top_of_surjective e.symm.surjective h

Affine Span Preservation under Affine Equivalence

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$, and let $e \colon P_1 \simeq P_2$ be an affine equivalence. For any subset $s \subseteq P_1$, the affine span of $s$ equals the entire space $P_1$ if and only if the affine span of the image $e(s)$ equals the entire space $P_2$. In symbols: $$\text{affineSpan}_k s = P_1 \leftrightarrow \text{affineSpan}_k e(s) = P_2.$$

AffineSubspace.comap definition

(f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₂) : AffineSubspace k P₁

Full source

/-- The preimage of an affine subspace under an affine map as an affine subspace. -/
def comap (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₂) : AffineSubspace k P₁ where
  carrier := f ⁻¹' s
  smul_vsub_vadd_mem t p₁ p₂ p₃ (hp₁ : f p₁ ∈ s) (hp₂ : f p₂ ∈ s) (hp₃ : f p₃ ∈ s) :=
    show f _ ∈ s by
      rw [AffineMap.map_vadd, LinearMap.map_smul, AffineMap.linearMap_vsub]
      apply s.smul_vsub_vadd_mem _ hp₁ hp₂ hp₃

Preimage of an affine subspace under an affine map

Informal description

Given an affine map $ f : P_1 \to P_2 $ between affine spaces over a ring $ k $, and an affine subspace $ s $ of $ P_2 $, the preimage $ \text{comap} f s $ is the affine subspace of $ P_1 $ consisting of all points $ x $ such that $ f(x) \in s $. More formally, the preimage is defined as the subset $ f^{-1}(s) $ of $ P_1 $, and it inherits the structure of an affine subspace by verifying that it is closed under affine combinations (i.e., for any three points $ p_1, p_2, p_3 $ in the preimage, the combination $ t \cdot (p_1 - p_2) + p_3 $ also lies in the preimage for any scalar $ t $).

AffineSubspace.coe_comap theorem

(f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₂) : (s.comap f : Set P₁) = f ⁻¹' ↑s

Full source

@[simp]
theorem coe_comap (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₂) : (s.comap f : Set P₁) = f ⁻¹' ↑s :=
  rfl

Preimage of Affine Subspace Under Affine Map Equals Set Preimage

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$, and let $f : P_1 \to P_2$ be an affine map. For any affine subspace $s$ of $P_2$, the underlying set of the preimage affine subspace $\text{comap}\, f\, s$ in $P_1$ is equal to the preimage $f^{-1}(s)$ of the underlying set of $s$ under $f$.

AffineSubspace.mem_comap theorem

{f : P₁ →ᵃ[k] P₂} {x : P₁} {s : AffineSubspace k P₂} : x ∈ s.comap f ↔ f x ∈ s

Full source

@[simp]
theorem mem_comap {f : P₁ →ᵃ[k] P₂} {x : P₁} {s : AffineSubspace k P₂} : x ∈ s.comap fx ∈ s.comap f ↔ f x ∈ s :=
  Iff.rfl

Characterization of Membership in Preimage Affine Subspace

Informal description

For an affine map $f \colon P_1 \to P_2$ between affine spaces over a ring $k$, a point $x \in P_1$, and an affine subspace $s$ of $P_2$, the point $x$ belongs to the preimage affine subspace $\text{comap}\,f\,s$ if and only if its image $f(x)$ belongs to $s$.

AffineSubspace.comap_mono theorem

{f : P₁ →ᵃ[k] P₂} {s t : AffineSubspace k P₂} : s ≤ t → s.comap f ≤ t.comap f

Full source

theorem comap_mono {f : P₁ →ᵃ[k] P₂} {s t : AffineSubspace k P₂} : s ≤ t → s.comap f ≤ t.comap f :=
  preimage_mono

Monotonicity of Affine Subspace Preimage under Inclusion

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$, and let $f \colon P_1 \to P_2$ be an affine map. For any two affine subspaces $s$ and $t$ of $P_2$ with $s \subseteq t$, the preimage affine subspace $\text{comap}\,f\,s$ is contained in the preimage affine subspace $\text{comap}\,f\,t$.

AffineSubspace.comap_top theorem

{f : P₁ →ᵃ[k] P₂} : (⊤ : AffineSubspace k P₂).comap f = ⊤

Full source

@[simp]
theorem comap_top {f : P₁ →ᵃ[k] P₂} : (⊤ : AffineSubspace k P₂).comap f = ⊤ := by
  rw [AffineSubspace.ext_iff]
  exact preimage_univ (f := f)

Preimage of Entire Affine Space is Entire Domain

Informal description

For any affine map $f \colon P_1 \to P_2$ between affine spaces over a ring $k$, the preimage of the top affine subspace (i.e., the entire space $P_2$) under $f$ is equal to the top affine subspace of $P_1$ (i.e., $P_1$ itself). In other words, $f^{-1}(P_2) = P_1$.

AffineSubspace.comap_bot theorem

(f : P₁ →ᵃ[k] P₂) : comap f ⊥ = ⊥

Full source

@[simp] theorem comap_bot (f : P₁ →ᵃ[k] P₂) : comap f ⊥ = ⊥ := rfl

Preimage of Trivial Affine Subspace is Trivial

Informal description

For any affine map $f \colon P_1 \to P_2$ between affine spaces over a ring $k$, the preimage of the trivial affine subspace $\bot$ of $P_2$ under $f$ is equal to the trivial affine subspace $\bot$ of $P_1$.

AffineSubspace.comap_id theorem

(s : AffineSubspace k P₁) : s.comap (AffineMap.id k P₁) = s

Full source

@[simp]
theorem comap_id (s : AffineSubspace k P₁) : s.comap (AffineMap.id k P₁) = s :=
  rfl

Preimage of Affine Subspace under Identity Map is Itself

Informal description

For any affine subspace $s$ of an affine space $P_1$ over a ring $k$, the preimage of $s$ under the identity affine map $\text{id} : P_1 \to P_1$ is equal to $s$ itself.

AffineSubspace.comap_comap theorem

 (s : AffineSubspace k P₃) (f : P₁ →ᵃ[k] P₂) (g : P₂ →ᵃ[k] P₃) : (s.comap g).comap f = s.comap (g.comp f)

Full source

theorem comap_comap (s : AffineSubspace k P₃) (f : P₁ →ᵃ[k] P₂) (g : P₂ →ᵃ[k] P₃) :
    (s.comap g).comap f = s.comap (g.comp f) :=
  rfl

Preimage of Preimage Equals Preimage of Composition for Affine Subspaces

Informal description

Let $P_1$, $P_2$, and $P_3$ be affine spaces over a ring $k$, and let $f \colon P_1 \to P_2$ and $g \colon P_2 \to P_3$ be affine maps. For any affine subspace $s$ of $P_3$, the preimage of $s$ under $g$ followed by the preimage under $f$ is equal to the preimage of $s$ under the composition $g \circ f$. In other words, $(g^{-1}(s))^{-1}(f) = (g \circ f)^{-1}(s)$.

AffineSubspace.map_le_iff_le_comap theorem

{f : P₁ →ᵃ[k] P₂} {s : AffineSubspace k P₁} {t : AffineSubspace k P₂} : s.map f ≤ t ↔ s ≤ t.comap f

Full source

theorem map_le_iff_le_comap {f : P₁ →ᵃ[k] P₂} {s : AffineSubspace k P₁} {t : AffineSubspace k P₂} :
    s.map f ≤ t ↔ s ≤ t.comap f :=
  image_subset_iff

Image-Preimage Inclusion Equivalence for Affine Subspaces

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$, and let $f \colon P_1 \to P_2$ be an affine map. For any affine subspaces $s$ of $P_1$ and $t$ of $P_2$, the image of $s$ under $f$ is contained in $t$ if and only if $s$ is contained in the preimage of $t$ under $f$. In symbols: \[ f(s) \subseteq t \leftrightarrow s \subseteq f^{-1}(t). \]

AffineSubspace.gc_map_comap theorem

(f : P₁ →ᵃ[k] P₂) : GaloisConnection (map f) (comap f)

Full source

theorem gc_map_comap (f : P₁ →ᵃ[k] P₂) : GaloisConnection (map f) (comap f) := fun _ _ =>
  map_le_iff_le_comap

Galois Connection Between Image and Preimage of Affine Subspaces

Informal description

For any affine map $f \colon P_1 \to P_2$ between affine spaces over a ring $k$, the pair of functions `map f` (image under $f$) and `comap f` (preimage under $f$) form a Galois connection between the complete lattices of affine subspaces of $P_1$ and $P_2$. This means that for any affine subspaces $s \subseteq P_1$ and $t \subseteq P_2$, we have: \[ f(s) \subseteq t \quad \text{if and only if} \quad s \subseteq f^{-1}(t). \]

AffineSubspace.map_comap_le theorem

(f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₂) : (s.comap f).map f ≤ s

Full source

theorem map_comap_le (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₂) : (s.comap f).map f ≤ s :=
  (gc_map_comap f).l_u_le _

Image of Preimage is Contained in Original Subspace

Informal description

For any affine map $f \colon P_1 \to P_2$ between affine spaces over a ring $k$, and any affine subspace $s$ of $P_2$, the image under $f$ of the preimage of $s$ under $f$ is contained in $s$. In symbols: \[ f(f^{-1}(s)) \subseteq s. \]

AffineSubspace.le_comap_map theorem

(f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₁) : s ≤ (s.map f).comap f

Full source

theorem le_comap_map (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₁) : s ≤ (s.map f).comap f :=
  (gc_map_comap f).le_u_l _

Subspace is Contained in Preimage of its Image under Affine Map

Informal description

For any affine map $f \colon P_1 \to P_2$ between affine spaces over a ring $k$, and any affine subspace $s$ of $P_1$, the subspace $s$ is contained in the preimage under $f$ of the image of $s$ under $f$. In symbols: \[ s \subseteq f^{-1}(f(s)). \]

AffineSubspace.map_sup theorem

(s t : AffineSubspace k P₁) (f : P₁ →ᵃ[k] P₂) : (s ⊔ t).map f = s.map f ⊔ t.map f

Full source

theorem map_sup (s t : AffineSubspace k P₁) (f : P₁ →ᵃ[k] P₂) : (s ⊔ t).map f = s.map f ⊔ t.map f :=
  (gc_map_comap f).l_sup

Image of Supremum of Affine Subspaces Equals Supremum of Images

Informal description

For any two affine subspaces $s$ and $t$ of an affine space $P_1$ over a ring $k$, and any affine map $f \colon P_1 \to P_2$, the image of the supremum (affine span of the union) of $s$ and $t$ under $f$ is equal to the supremum of the images of $s$ and $t$ under $f$. In symbols: \[ f(s \sqcup t) = f(s) \sqcup f(t). \]

AffineSubspace.map_iSup theorem

{ι : Sort*} (f : P₁ →ᵃ[k] P₂) (s : ι → AffineSubspace k P₁) : (iSup s).map f = ⨆ i, (s i).map f

Full source

theorem map_iSup {ι : Sort*} (f : P₁ →ᵃ[k] P₂) (s : ι → AffineSubspace k P₁) :
    (iSup s).map f = ⨆ i, (s i).map f :=
  (gc_map_comap f).l_iSup

Image of Affine Span Under Affine Map Equals Affine Span of Images

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$, and let $f \colon P_1 \to P_2$ be an affine map. For any family of affine subspaces $\{s_i\}_{i \in \iota}$ of $P_1$, the image under $f$ of the supremum (affine span of the union) of the $s_i$ equals the supremum of the images $f(s_i)$. In symbols: \[ f\left(\bigsqcup_{i \in \iota} s_i\right) = \bigsqcup_{i \in \iota} f(s_i). \]

AffineSubspace.comap_inf theorem

(s t : AffineSubspace k P₂) (f : P₁ →ᵃ[k] P₂) : (s ⊓ t).comap f = s.comap f ⊓ t.comap f

Full source

theorem comap_inf (s t : AffineSubspace k P₂) (f : P₁ →ᵃ[k] P₂) :
    (s ⊓ t).comap f = s.comap f ⊓ t.comap f :=
  (gc_map_comap f).u_inf

Preimage of Intersection of Affine Subspaces Equals Intersection of Preimages

Informal description

For any two affine subspaces $s$ and $t$ of an affine space $P_2$ over a ring $k$, and any affine map $f \colon P_1 \to P_2$ between affine spaces, the preimage of the intersection $s \cap t$ under $f$ is equal to the intersection of the preimages of $s$ and $t$ under $f$. In other words, $f^{-1}(s \cap t) = f^{-1}(s) \cap f^{-1}(t)$.

AffineSubspace.comap_supr theorem

{ι : Sort*} (f : P₁ →ᵃ[k] P₂) (s : ι → AffineSubspace k P₂) : (iInf s).comap f = ⨅ i, (s i).comap f

Full source

theorem comap_supr {ι : Sort*} (f : P₁ →ᵃ[k] P₂) (s : ι → AffineSubspace k P₂) :
    (iInf s).comap f = ⨅ i, (s i).comap f :=
  (gc_map_comap f).u_iInf

Preimage of Infimum of Affine Subspaces Equals Infimum of Preimages

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$, and let $f \colon P_1 \to P_2$ be an affine map. For any family of affine subspaces $(s_i)_{i \in \iota}$ of $P_2$, the preimage under $f$ of their infimum equals the infimum of their preimages: \[ f^{-1}\left(\bigsqcap_{i \in \iota} s_i\right) = \bigsqcap_{i \in \iota} f^{-1}(s_i). \]

AffineSubspace.comap_symm theorem

(e : P₁ ≃ᵃ[k] P₂) (s : AffineSubspace k P₁) : s.comap (e.symm : P₂ →ᵃ[k] P₁) = s.map e

Full source

@[simp]
theorem comap_symm (e : P₁ ≃ᵃ[k] P₂) (s : AffineSubspace k P₁) :
    s.comap (e.symm : P₂ →ᵃ[k] P₁) = s.map e :=
  coe_injective <| e.preimage_symm _

Preimage-Image Symmetry for Affine Subspaces under Affine Equivalence

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$, and let $e : P_1 \simeq P_2$ be an affine equivalence between them. For any affine subspace $s$ of $P_1$, the preimage of $s$ under the inverse affine map $e^{-1} : P_2 \to P_1$ equals the image of $s$ under $e$. In other words, $(e^{-1})^{-1}(s) = e(s)$ for any affine subspace $s \subseteq P_1$.

AffineSubspace.map_symm theorem

(e : P₁ ≃ᵃ[k] P₂) (s : AffineSubspace k P₂) : s.map (e.symm : P₂ →ᵃ[k] P₁) = s.comap e

Full source

@[simp]
theorem map_symm (e : P₁ ≃ᵃ[k] P₂) (s : AffineSubspace k P₂) :
    s.map (e.symm : P₂ →ᵃ[k] P₁) = s.comap e :=
  coe_injective <| e.image_symm _

Image-Preimage Symmetry for Affine Subspaces under Affine Equivalence

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$, and let $e : P_1 \simeq P_2$ be an affine equivalence between them. For any affine subspace $s$ of $P_2$, the image of $s$ under the inverse affine map $e^{-1} : P_2 \to P_1$ equals the preimage of $s$ under $e$. In other words, $e^{-1}(s) = e^{-1}(s)$ for any affine subspace $s \subseteq P_2$.

AffineSubspace.comap_span theorem

(f : P₁ ≃ᵃ[k] P₂) (s : Set P₂) : (affineSpan k s).comap (f : P₁ →ᵃ[k] P₂) = affineSpan k (f ⁻¹' s)

Full source

theorem comap_span (f : P₁ ≃ᵃ[k] P₂) (s : Set P₂) :
    (affineSpan k s).comap (f : P₁ →ᵃ[k] P₂) = affineSpan k (f ⁻¹' s) := by
  rw [← map_symm, map_span, AffineEquiv.coe_coe, f.image_symm]

Affine Span Commutes with Preimages under Affine Equivalence

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$, and let $f : P_1 \simeq P_2$ be an affine equivalence between them. For any subset $s \subseteq P_2$, the preimage of the affine span of $s$ under $f$ is equal to the affine span of the preimage of $s$ under $f$. In symbols: $$ f^{-1}(\text{affineSpan}_k s) = \text{affineSpan}_k (f^{-1}(s)). $$

AffineSubspace.Parallel definition

(s₁ s₂ : AffineSubspace k P) : Prop

Full source

/-- Two affine subspaces are parallel if one is related to the other by adding the same vector
to all points. -/
def Parallel (s₁ s₂ : AffineSubspace k P) : Prop :=
  ∃ v : V, s₂ = s₁.map (constVAdd k P v)

Parallel affine subspaces

Informal description

Two affine subspaces $ s_1 $ and $ s_2 $ of an affine space $ P $ over a module $ V $ with scalar ring $ k $ are *parallel* if there exists a vector $ v \in V $ such that $ s_2 $ is the image of $ s_1 $ under the translation by $ v $. In other words, $ s_2 $ is obtained by adding the same vector $ v $ to all points in $ s_1 $.

Affine.term_∥_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
scoped[Affine] infixl:50 " ∥ " => AffineSubspace.Parallel

Parallel relation between affine subspaces

Informal description

The infix notation `∥` denotes the parallel relation between two affine subspaces, where two subspaces are parallel if one is a translate of the other.

AffineSubspace.Parallel.symm theorem

{s₁ s₂ : AffineSubspace k P} (h : s₁ ∥ s₂) : s₂ ∥ s₁

Full source

@[symm]
theorem Parallel.symm {s₁ s₂ : AffineSubspace k P} (h : s₁ ∥ s₂) : s₂ ∥ s₁ := by
  rcases h with ⟨v, rfl⟩
  refine ⟨-v, ?_⟩
  rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add, neg_add_cancel, constVAdd_zero,
    coe_refl_to_affineMap, map_id]

Symmetry of Parallel Relation for Affine Subspaces

Informal description

For any two affine subspaces $ s_1 $ and $ s_2 $ of an affine space $ P $ over a module $ V $ with scalar ring $ k $, if $ s_1 $ is parallel to $ s_2 $, then $ s_2 $ is parallel to $ s_1 $.

AffineSubspace.parallel_comm theorem

{s₁ s₂ : AffineSubspace k P} : s₁ ∥ s₂ ↔ s₂ ∥ s₁

Full source

theorem parallel_comm {s₁ s₂ : AffineSubspace k P} : s₁ ∥ s₂s₁ ∥ s₂ ↔ s₂ ∥ s₁ :=
  ⟨Parallel.symm, Parallel.symm⟩

Commutativity of Parallel Relation for Affine Subspaces

Informal description

For any two affine subspaces $ s_1 $ and $ s_2 $ of an affine space $ P $ over a module $ V $ with scalar ring $ k $, $ s_1 $ is parallel to $ s_2 $ if and only if $ s_2 $ is parallel to $ s_1 $.

AffineSubspace.Parallel.refl theorem

(s : AffineSubspace k P) : s ∥ s

Full source

@[refl]
theorem Parallel.refl (s : AffineSubspace k P) : s ∥ s :=
  ⟨0, by simp⟩

Reflexivity of Parallel Relation for Affine Subspaces

Informal description

For any affine subspace $s$ of an affine space $P$ over a module $V$ with scalar ring $k$, $s$ is parallel to itself.

AffineSubspace.Parallel.trans theorem

{s₁ s₂ s₃ : AffineSubspace k P} (h₁₂ : s₁ ∥ s₂) (h₂₃ : s₂ ∥ s₃) : s₁ ∥ s₃

Full source

@[trans]
theorem Parallel.trans {s₁ s₂ s₃ : AffineSubspace k P} (h₁₂ : s₁ ∥ s₂) (h₂₃ : s₂ ∥ s₃) :
    s₁ ∥ s₃ := by
  rcases h₁₂ with ⟨v₁₂, rfl⟩
  rcases h₂₃ with ⟨v₂₃, rfl⟩
  refine ⟨v₂₃ + v₁₂, ?_⟩
  rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add]

Transitivity of Parallel Relation for Affine Subspaces

Informal description

Let $s_1$, $s_2$, and $s_3$ be affine subspaces of an affine space $P$ over a module $V$ with scalar ring $k$. If $s_1$ is parallel to $s_2$ and $s_2$ is parallel to $s_3$, then $s_1$ is parallel to $s_3$.

AffineSubspace.Parallel.direction_eq theorem

{s₁ s₂ : AffineSubspace k P} (h : s₁ ∥ s₂) : s₁.direction = s₂.direction

Full source

theorem Parallel.direction_eq {s₁ s₂ : AffineSubspace k P} (h : s₁ ∥ s₂) :
    s₁.direction = s₂.direction := by
  rcases h with ⟨v, rfl⟩
  simp

Parallel Affine Subspaces Have Equal Directions

Informal description

For any two affine subspaces $ s_1 $ and $ s_2 $ of an affine space $ P $ over a module $ V $ with scalar ring $ k $, if $ s_1 $ is parallel to $ s_2 $, then their direction submodules are equal, i.e., $ \text{direction}(s_1) = \text{direction}(s_2) $.

AffineSubspace.parallel_bot_iff_eq_bot theorem

{s : AffineSubspace k P} : s ∥ ⊥ ↔ s = ⊥

Full source

@[simp]
theorem parallel_bot_iff_eq_bot {s : AffineSubspace k P} : s ∥ ⊥s ∥ ⊥ ↔ s = ⊥ := by
  refine ⟨fun h => ?_, fun h => h ▸ Parallel.refl _⟩
  rcases h with ⟨v, h⟩
  rwa [eq_comm, map_eq_bot_iff] at h

Parallel to Empty Subspace iff Empty

Informal description

An affine subspace $s$ of an affine space $P$ over a module $V$ with scalar ring $k$ is parallel to the empty affine subspace if and only if $s$ itself is the empty affine subspace. In symbols: $$ s \parallel \bot \leftrightarrow s = \bot. $$

AffineSubspace.bot_parallel_iff_eq_bot theorem

{s : AffineSubspace k P} : ⊥ ∥ s ↔ s = ⊥

Full source

@[simp]
theorem bot_parallel_iff_eq_bot {s : AffineSubspace k P} : ⊥⊥ ∥ s⊥ ∥ s ↔ s = ⊥ := by
  rw [parallel_comm, parallel_bot_iff_eq_bot]

Empty Subspace Parallel iff Subspace is Empty

Informal description

The empty affine subspace $\bot$ is parallel to an affine subspace $s$ of an affine space $P$ over a module $V$ with scalar ring $k$ if and only if $s$ is itself the empty affine subspace. In symbols: $$ \bot \parallel s \leftrightarrow s = \bot. $$

AffineSubspace.parallel_iff_direction_eq_and_eq_bot_iff_eq_bot theorem

{s₁ s₂ : AffineSubspace k P} : s₁ ∥ s₂ ↔ s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)

Full source

theorem parallel_iff_direction_eq_and_eq_bot_iff_eq_bot {s₁ s₂ : AffineSubspace k P} :
    s₁ ∥ s₂s₁ ∥ s₂ ↔ s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥) := by
  refine ⟨fun h => ⟨h.direction_eq, ?_, ?_⟩, fun h => ?_⟩
  · rintro rfl
    exact bot_parallel_iff_eq_bot.1 h
  · rintro rfl
    exact parallel_bot_iff_eq_bot.1 h
  · rcases h with ⟨hd, hb⟩
    by_cases hs₁ : s₁ = ⊥
    · rw [hs₁, bot_parallel_iff_eq_bot]
      exact hb.1 hs₁
    · have hs₂ : s₂ ≠ ⊥ := hb.not.1 hs₁
      rcases (nonempty_iff_ne_bot s₁).2 hs₁ with ⟨p₁, hp₁⟩
      rcases (nonempty_iff_ne_bot s₂).2 hs₂ with ⟨p₂, hp₂⟩
      refine ⟨p₂ -ᵥ p₁, (eq_iff_direction_eq_of_mem hp₂ ?_).2 ?_⟩
      · rw [mem_map]
        refine ⟨p₁, hp₁, ?_⟩
        simp
      · simpa using hd.symm

Characterization of Parallel Affine Subspaces via Directions and Emptiness

Informal description

Two affine subspaces $ s_1 $ and $ s_2 $ of an affine space $ P $ over a module $ V $ with scalar ring $ k $ are parallel if and only if their direction submodules are equal and $ s_1 $ is the empty subspace if and only if $ s_2 $ is the empty subspace. In symbols: \[ s_1 \parallel s_2 \leftrightarrow \text{direction}(s_1) = \text{direction}(s_2) \land (s_1 = \bot \leftrightarrow s_2 = \bot). \]

AffineSubspace.Parallel.vectorSpan_eq theorem

{s₁ s₂ : Set P} (h : affineSpan k s₁ ∥ affineSpan k s₂) : vectorSpan k s₁ = vectorSpan k s₂

Full source

theorem Parallel.vectorSpan_eq {s₁ s₂ : Set P} (h : affineSpanaffineSpan k s₁ ∥ affineSpan k s₂) :
    vectorSpan k s₁ = vectorSpan k s₂ := by
  simp_rw [← direction_affineSpan]
  exact h.direction_eq

Equality of Vector Spans for Parallel Affine Spans

Informal description

For any two sets $s_1$ and $s_2$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, if the affine spans of $s_1$ and $s_2$ are parallel, then their vector spans are equal, i.e., $\text{vectorSpan}_k(s_1) = \text{vectorSpan}_k(s_2)$.

AffineSubspace.affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty theorem

 {s₁ s₂ : Set P} : affineSpan k s₁ ∥ affineSpan k s₂ ↔ vectorSpan k s₁ = vectorSpan k s₂ ∧ (s₁ = ∅ ↔ s₂ = ∅)

Full source

theorem affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty {s₁ s₂ : Set P} :
    affineSpanaffineSpan k s₁ ∥ affineSpan k s₂affineSpan k s₁ ∥ affineSpan k s₂ ↔ vectorSpan k s₁ = vectorSpan k s₂ ∧ (s₁ = ∅ ↔ s₂ = ∅) := by
  repeat rw [← direction_affineSpan, ← affineSpan_eq_bot k]
  exact parallel_iff_direction_eq_and_eq_bot_iff_eq_bot

Parallel Affine Spans via Vector Span Equality and Emptiness Condition

Informal description

For any two sets $s_1$ and $s_2$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, the affine spans of $s_1$ and $s_2$ are parallel if and only if their vector spans are equal and $s_1$ is empty if and only if $s_2$ is empty. In symbols: \[ \text{affineSpan}_k(s_1) \parallel \text{affineSpan}_k(s_2) \leftrightarrow \text{vectorSpan}_k(s_1) = \text{vectorSpan}_k(s_2) \land (s_1 = \emptyset \leftrightarrow s_2 = \emptyset). \]

AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq theorem

 {p₁ p₂ p₃ p₄ : P} :
  line[k, p₁, p₂] ∥ line[k, p₃, p₄] ↔ vectorSpan k ({ p₁, p₂ } : Set P) = vectorSpan k ({ p₃, p₄ } : Set P)

Full source

theorem affineSpan_pair_parallel_iff_vectorSpan_eq {p₁ p₂ p₃ p₄ : P} :
    line[k, p₁, p₂]line[k, p₁, p₂] ∥ line[k, p₃, p₄]line[k, p₁, p₂] ∥ line[k, p₃, p₄] ↔
      vectorSpan k ({p₁, p₂} : Set P) = vectorSpan k ({p₃, p₄} : Set P) := by
  simp [affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty, ←
    not_nonempty_iff_eq_empty]

Parallel Affine Lines via Vector Span Equality

Informal description

For any four points $p_1, p_2, p_3, p_4$ in an affine space $P$ over a module $V$ with scalar ring $k$, the affine line through $p_1$ and $p_2$ is parallel to the affine line through $p_3$ and $p_4$ if and only if the vector span of $\{p_1, p_2\}$ is equal to the vector span of $\{p_3, p_4\}$.

Main definitions