# 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.
theorem 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] [] [] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {E : } [Ene : Nonempty { x : P₁ // x E }] {φ : P₁ →ᵃ[k] P₂} :
Nonempty { x : P₂ // x }
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] [] [] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (φ : P₁ →ᵃ[k] P₂) {E : } {F : } [Nonempty { x : P₁ // x E }] [Nonempty { x : P₂ // x F }] (hEF : F) :
{ x : P₁ // x E } →ᵃ[k] { x : P₂ // x F }

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

Equations
• φ.restrict hEF = { toFun := fun (x : { x : P₁ // x E }) => φ x, , linear := φ.linear.restrict , map_vadd' := }
Instances For
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] [] [] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (φ : P₁ →ᵃ[k] P₂) {E : } {F : } [Nonempty { x : P₁ // x E }] [Nonempty { x : P₂ // x F }] (hEF : F) (x : { x : P₁ // 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] [] [] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} {E : } {F : } (hEF : 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] [] [] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (φ : P₁ →ᵃ[k] P₂) {E : } {F : } [Nonempty { x : P₁ // x E }] [Nonempty { x : P₂ // x F }] (hEF : 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] [] [] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : ) {E : } {F : } [Nonempty { x : P₁ // x E }] [Nonempty { x : P₂ // x F }] (hEF : 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] [] [] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (φ : P₁ →ᵃ[k] P₂) {E : } {F : } [Nonempty { x : P₁ // x E }] [Nonempty { x : P₂ // x F }] (h : = 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] [] [] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {E : } [Nonempty { x : P₁ // x E }] {φ : P₁ →ᵃ[k] P₂} (hφ : ) :
Function.Bijective (φ.restrict )