Range of affine maps

The range of an affine map f : P₁ →ᵃ[R] P₂ is an affine subspace of P₂.

Implementation note

Follows LinearMap.range.

def AffineMap.range {R : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [Ring R] [AddCommGroup V₁] [Module R V₁] [AddCommGroup V₂] [Module R V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) : AffineSubspace R P₂

The range of an affine map is an affine subspace.

Equations

• f.range = { carrier := Set.range ⇑f, smul_vsub_vadd_mem' := ⋯ }

instance AffineMap.instNonemptyRange {R : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [Ring R] [AddCommGroup V₁] [Module R V₁] [AddCommGroup V₂] [Module R V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) : Nonempty ↥f.range

The range of an affine map is nonempty.

@[simp]

theorem AffineMap.coe_range {R : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [Ring R] [AddCommGroup V₁] [Module R V₁] [AddCommGroup V₂] [Module R V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) : ↑f.range = Set.range ⇑f

@[simp]

theorem AffineMap.mem_range {R : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [Ring R] [AddCommGroup V₁] [Module R V₁] [AddCommGroup V₂] [Module R V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) (x : P₂) : x ∈ f.range ↔ ∃ (y : P₁), f y = x

@[simp]

theorem AffineMap.map_top {R : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [Ring R] [AddCommGroup V₁] [Module R V₁] [AddCommGroup V₂] [Module R V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) : AffineSubspace.map f ⊤ = f.range

theorem AffineMap.mem_range_self {R : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [Ring R] [AddCommGroup V₁] [Module R V₁] [AddCommGroup V₂] [Module R V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) (x : P₁) : f x ∈ f.range

@[simp]

theorem AffineMap.range_id {R : Type u_1} {V₁ : Type u_2} {P₁ : Type u_4} [Ring R] [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁] : (id R P₁).range = ⊤

theorem AffineMap.direction_range_eq_range_linear {R : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [Ring R] [AddCommGroup V₁] [Module R V₁] [AddCommGroup V₂] [Module R V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) : f.range.direction = f.linear.range

theorem AffineMap.range_eq_top_iff_surjective {R : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [Ring R] [AddCommGroup V₁] [Module R V₁] [AddCommGroup V₂] [Module R V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) : f.range = ⊤ ↔ Function.Surjective ⇑f

def AffineMap.rangeRestrict {R : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [Ring R] [AddCommGroup V₁] [Module R V₁] [AddCommGroup V₂] [Module R V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) : P₁ →ᵃ[R] ↥f.range

Restrict the codomain of an affine map f to f.range.

Equations

• f.rangeRestrict = { toFun := fun (p : P₁) => ⟨f p, ⋯⟩, linear := LinearMap.codRestrict f.range.direction f.linear ⋯, map_vadd' := ⋯ }

@[simp]

theorem AffineMap.rangeRestrict_linear_apply_coe {R : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [Ring R] [AddCommGroup V₁] [Module R V₁] [AddCommGroup V₂] [Module R V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) (c : V₁) : ↑(f.rangeRestrict.linear c) = f.linear c

@[simp]

theorem AffineMap.rangeRestrict_apply_coe {R : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [Ring R] [AddCommGroup V₁] [Module R V₁] [AddCommGroup V₂] [Module R V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) (p : P₁) : ↑(f.rangeRestrict p) = f p

theorem AffineMap.surjective_rangeRestrict {R : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [Ring R] [AddCommGroup V₁] [Module R V₁] [AddCommGroup V₂] [Module R V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) : Function.Surjective ⇑f.rangeRestrict

@[simp]

theorem AffineMap.range_rangeRestrict {R : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [Ring R] [AddCommGroup V₁] [Module R V₁] [AddCommGroup V₂] [Module R V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) : f.rangeRestrict.range = ⊤

@[simp]

theorem AffineMap.injective_rangeRestrict_iff {R : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [Ring R] [AddCommGroup V₁] [Module R V₁] [AddCommGroup V₂] [Module R V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) : Function.Injective ⇑f.rangeRestrict ↔ Function.Injective ⇑f