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₂]
[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₂} :
nonempty ↥(affine_subspace.map φ E)
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.
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) :
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) :
E.direction ≤ submodule.comap φ.linear F.direction
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) :
function.injective ⇑(φ.restrict hEF)
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) :
function.surjective ⇑(φ.restrict _)
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 ⇑φ) :
function.bijective ⇑(φ.restrict _)