Shifting an affine subspace towards a point

This file introduces a "shift" transformation of affine subspace, where the subspace is translated relatively to a point c. This is equivalent to AffineSubspace.map (AffineEquiv.constVAdd ..), but hides the detail of arbitrarily choosing a point in the subspace.

Shifting is controlled by a parameter r, indicating how far the output space is to c. We set r = 0 to mean the output space passes through c (See AffineSubspace.shift_zero), while r = 1 means not moving the input space at all (See AffineSubspace.shift_one). With this convention, this transformation is also equivalent to AffineSubspace.map (homothety c r) when r is a unit.

Main declarations

• AffineSubspace.shift defines the shift transformation.
• AffineSubspace.shift_eq shows the shift transformation is equivalent to translation.
• AffineSubspace.shift_eq_map_homothety shows the shift transformation is equivalent to homothety.

noncomputable def AffineSubspace.shift {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [AddTorsor V P] [Module k V] (s : AffineSubspace k P) (c : P) (r : k) : AffineSubspace k P

AffineSubspace.shift s c r is an affine subspace parallel to s, where an arbitrary point on s is moved towards c with linear interpolation by r. When r = 0, that point is moved onto c. When r = 1, that point stays at the original position. A different choice of the point will not affect the output (See AffineSubspace.shift_eq).

We define AffineSubspace.shift ⊥ c r = ⊥ (See AffineSubspace.shift_bot).

Equations

• s.shift c r = if h : Nonempty ↥s then AffineSubspace.map (↑(AffineEquiv.constVAdd k P ((1 - r) • (c -ᵥ ↑h.some)))) s else ⊥

@[simp]

theorem AffineSubspace.direction_shift {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [AddTorsor V P] [Module k V] (s : AffineSubspace k P) (c : P) (r : k) : (s.shift c r).direction = s.direction

@[simp]

theorem AffineSubspace.shift_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [AddTorsor V P] [Module k V] (c : P) (r : k) : ⊤.shift c r = ⊤

@[simp]

theorem AffineSubspace.shift_bot {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [AddTorsor V P] [Module k V] (c : P) (r : k) : ⊥.shift c r = ⊥

theorem AffineSubspace.shift_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [AddTorsor V P] [Module k V] {s : AffineSubspace k P} (p : ↥s) (c : P) (r : k) : s.shift c r = map (↑(AffineEquiv.constVAdd k P ((1 - r) • (c -ᵥ ↑p)))) s

AffineSubspace.shift s c r can be represented by moving a point in the subspace towards c.

@[simp]

theorem AffineSubspace.shift_zero {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [AddTorsor V P] [Module k V] (s : AffineSubspace k P) [h : Nonempty ↥s] (c : P) : s.shift c 0 = mk' c s.direction

@[simp]

theorem AffineSubspace.shift_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [AddTorsor V P] [Module k V] (s : AffineSubspace k P) (c : P) : s.shift c 1 = s

theorem AffineSubspace.shift_eq_map_homothety {k : Type u_1} {V : Type u_2} {P : Type u_3} [CommRing k] [AddCommGroup V] [AddTorsor V P] [Module k V] (s : AffineSubspace k P) (c : P) {r : k} (hr : IsUnit r) : s.shift c r = map (AffineMap.homothety c r) s

For a unit parameter, shifting is the same as mapping by homothety.