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]
[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 ↥(AffineSubspace.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)
:
Restrict domain and codomain of an affine map to the given subspaces.
Equations
- AffineMap.restrict φ hEF = { toFun := fun (x : ↥E) => { val := φ ↑x, property := ⋯ }, linear := LinearMap.restrict φ.linear ⋯, 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]
[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)
:
↑((AffineMap.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)
:
AffineSubspace.direction E ≤ Submodule.comap φ.linear (AffineSubspace.direction F)
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)
:
(AffineMap.restrict φ hEF).linear = LinearMap.restrict φ.linear ⋯
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 ⇑(AffineMap.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)
:
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 ⇑φ)
: