# mathlib3documentation

linear_algebra.affine_space.restrict

# Affine map restrictions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines restrictions of affine maps.

## Main definitions #

• The domain and codomain of an affine map can be restricted using affine_map.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 affine_subspace.nonempty_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [add_comm_group V₂] [ V₁] [ V₂] [ P₁] [ P₂] {E : P₁} [Ene : nonempty E] {φ : P₁ →ᵃ[k] P₂} :
def affine_map.restrict {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [add_comm_group V₂] [ V₁] [ V₂] [ P₁] [ P₂] (φ : P₁ →ᵃ[k] P₂) {E : P₁} {F : P₂} [nonempty E] [nonempty F] (hEF : F) :

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

Equations
theorem affine_map.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] [add_comm_group V₁] [add_comm_group V₂] [ V₁] [ V₂] [ P₁] [ P₂] (φ : P₁ →ᵃ[k] P₂) {E : P₁} {F : P₂} [nonempty E] [nonempty F] (hEF : F) (x : E) :
((φ.restrict hEF) x) = φ x
theorem affine_map.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] [add_comm_group V₁] [add_comm_group V₂] [ V₁] [ V₂] [ P₁] [ P₂] {φ : P₁ →ᵃ[k] P₂} {E : P₁} {F : P₂} (hEF : F) :
theorem affine_map.restrict.linear {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [add_comm_group V₂] [ V₁] [ V₂] [ P₁] [ P₂] (φ : P₁ →ᵃ[k] P₂) {E : P₁} {F : P₂} [nonempty E] [nonempty F] (hEF : F) :
theorem affine_map.restrict.injective {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [add_comm_group V₂] [ V₁] [ V₂] [ P₁] [ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : function.injective φ) {E : P₁} {F : P₂} [nonempty E] [nonempty F] (hEF : F) :
theorem affine_map.restrict.surjective {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [add_comm_group V₂] [ V₁] [ V₂] [ P₁] [ P₂] (φ : P₁ →ᵃ[k] P₂) {E : P₁} {F : P₂} [nonempty E] [nonempty F] (h : = F) :
theorem affine_map.restrict.bijective {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [add_comm_group V₂] [ V₁] [ V₂] [ P₁] [ P₂] {E : P₁} [nonempty E] {φ : P₁ →ᵃ[k] P₂} (hφ : function.injective φ) :