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
- φ.restrict hEF = { toFun := fun (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]
[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)
:
↑((φ.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)
:
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]
[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 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]
[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 ⇑(φ.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)
:
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]
[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 ⇑φ)
:
Function.Bijective ⇑(φ.restrict ⋯)