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 { x // x ∈ E }]
{φ : P₁ →ᵃ[k] P₂}
:
Nonempty { x // x ∈ 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 { x // x ∈ E }]
[Nonempty { x // x ∈ F }]
(hEF : AffineSubspace.map φ E ≤ F)
:
Restrict domain and codomain of an affine map to the given subspaces.
Equations
- One or more equations did not get rendered due to their size.
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 { x // x ∈ E }]
[Nonempty { x // x ∈ F }]
(hEF : AffineSubspace.map φ E ≤ F)
(x : { x // 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 { x // x ∈ E }]
[Nonempty { x // x ∈ F }]
(hEF : AffineSubspace.map φ E ≤ F)
:
(AffineMap.restrict φ hEF).linear = LinearMap.restrict φ.linear (_ : AffineSubspace.direction E ≤ Submodule.comap φ.linear (AffineSubspace.direction F))
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 { x // x ∈ E }]
[Nonempty { x // x ∈ 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 { x // x ∈ E }]
[Nonempty { x // x ∈ F }]
(h : AffineSubspace.map φ E = F)
:
Function.Surjective ↑(AffineMap.restrict φ (_ : 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 { x // x ∈ E }]
{φ : P₁ →ᵃ[k] P₂}
(hφ : Function.Injective ↑φ)
:
Function.Bijective ↑(AffineMap.restrict φ (_ : AffineSubspace.map φ E ≤ AffineSubspace.map φ E))