mathlib3 documentation

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 #

Main theorems #

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₂] [module k V₁] [module k V₂] [add_torsor V₁ P₁] [add_torsor V₂ P₂] {E : affine_subspace k 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₂] [module k V₁] [module k V₂] [add_torsor V₁ P₁] [add_torsor V₂ P₂] (φ : P₁ →ᵃ[k] P₂) {E : affine_subspace k P₁} {F : affine_subspace k P₂} [nonempty E] [nonempty F] (hEF : affine_subspace.map φ E 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₂] [module k V₁] [module k V₂] [add_torsor V₁ P₁] [add_torsor V₂ P₂] (φ : P₁ →ᵃ[k] P₂) {E : affine_subspace k P₁} {F : affine_subspace k P₂} [nonempty E] [nonempty F] (hEF : affine_subspace.map φ E 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₂] [module k V₁] [module k V₂] [add_torsor V₁ P₁] [add_torsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} {E : affine_subspace k P₁} {F : affine_subspace k P₂} (hEF : affine_subspace.map φ E 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₂] [module k V₁] [module k V₂] [add_torsor V₁ P₁] [add_torsor V₂ P₂] (φ : P₁ →ᵃ[k] P₂) {E : affine_subspace k P₁} {F : affine_subspace k P₂} [nonempty E] [nonempty F] (hEF : affine_subspace.map φ E 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₂] [module k V₁] [module k V₂] [add_torsor V₁ P₁] [add_torsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : function.injective φ) {E : affine_subspace k P₁} {F : affine_subspace k P₂} [nonempty E] [nonempty F] (hEF : affine_subspace.map φ E 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₂] [module k V₁] [module k V₂] [add_torsor V₁ P₁] [add_torsor V₂ P₂] (φ : P₁ →ᵃ[k] P₂) {E : affine_subspace k P₁} {F : affine_subspace k P₂} [nonempty E] [nonempty F] (h : affine_subspace.map φ E = 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₂] [module k V₁] [module k V₂] [add_torsor V₁ P₁] [add_torsor V₂ P₂] {E : affine_subspace k P₁} [nonempty E] {φ : P₁ →ᵃ[k] P₂} (hφ : function.injective φ) :