Affine map restrictions

This file defines restrictions of affine maps.

Main definitions

• The domain and codomain of an affine map can be restricted using AffineMap.restrict.

Main theorems

• The associated linear map of the restriction is the restriction of the linear map associated to the original affine map.
• The restriction is injective if the original map is injective.
• The restriction in surjective if the codomain is the image of the domain.

instance AffineSubspace.nonempty_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {E : AffineSubspace k P₁} [Ene : Nonempty ↥E] {φ : P₁ →ᵃ[k] P₂} : Nonempty ↥(map φ E)

def AffineMap.restrict {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (φ : P₁ →ᵃ[k] P₂) {E : AffineSubspace k P₁} {F : AffineSubspace k P₂} [Nonempty ↥E] [Nonempty ↥F] (hEF : AffineSubspace.map φ E ≤ F) : ↥E →ᵃ[k] ↥F

Restrict domain and codomain of an affine map to the given subspaces.

Equations

• φ.restrict hEF = { toFun := fun (x : ↥E) => ⟨φ ↑x, ⋯⟩, linear := φ.linear.restrict ⋯, map_vadd' := ⋯ }

theorem AffineMap.restrict.coe_apply {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (φ : P₁ →ᵃ[k] P₂) {E : AffineSubspace k P₁} {F : AffineSubspace k P₂} [Nonempty ↥E] [Nonempty ↥F] (hEF : AffineSubspace.map φ E ≤ F) (x : ↥E) : ↑((φ.restrict hEF) x) = φ ↑x

theorem AffineMap.restrict.linear_aux {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} {E : AffineSubspace k P₁} {F : AffineSubspace k P₂} (hEF : AffineSubspace.map φ E ≤ F) : E.direction ≤ Submodule.comap φ.linear F.direction

theorem AffineMap.restrict.linear {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (φ : P₁ →ᵃ[k] P₂) {E : AffineSubspace k P₁} {F : AffineSubspace k P₂} [Nonempty ↥E] [Nonempty ↥F] (hEF : AffineSubspace.map φ E ≤ F) : (φ.restrict hEF).linear = φ.linear.restrict ⋯

theorem AffineMap.restrict.injective {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Injective ⇑φ) {E : AffineSubspace k P₁} {F : AffineSubspace k P₂} [Nonempty ↥E] [Nonempty ↥F] (hEF : AffineSubspace.map φ E ≤ F) : Function.Injective ⇑(φ.restrict hEF)

theorem AffineMap.restrict.surjective {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (φ : P₁ →ᵃ[k] P₂) {E : AffineSubspace k P₁} {F : AffineSubspace k P₂} [Nonempty ↥E] [Nonempty ↥F] (h : AffineSubspace.map φ E = F) : Function.Surjective ⇑(φ.restrict ⋯)

theorem AffineMap.restrict.bijective {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {E : AffineSubspace k P₁} [Nonempty ↥E] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Injective ⇑φ) : Function.Bijective ⇑(φ.restrict ⋯)