Homogenization of an affine space

The homogenization (or vector hull) of an affine space P is a vector space together with an embedding of P as a hyperplane not passing through the origin. This construction has the universal property that every affine map defined on this hyperplane that takes values in a vector space can be uniquely extended to a linear map defined on the homogenization.

Note that the homogenization is isomorphic to V × R, where V is the vector space associated to P and R is the ring of scalars. However, this isomorphism is not canonical unless P = V (see Homogenization.toProd in this case).

Main definitions

• Homogenization R P: the homogenization of the affine space P over the ring R.
• Homogenization.ofPoint: the canonical embedding of the affine space.
• Homogenization.ofVector: the canonical embedding of the vector space.
• Homogenization.lift f: the linear map obtained by extending the affine map f taking values in a vector space.

References

• J. Gallier, Geometric Methods and Applications for Computer Science and Engineering
• X. Gràcia, R. Martín, Vector Hulls of Affine Spaces and Affine Bundles

def Homogenization (R : Type u_1) {V : Type u_2} (P : Type u_3) [Ring R] [AddCommGroup V] [Module R V] [AddTorsor V P] : Type (max u_2 u_1)

Given an affine space P over R, Homogenization R P is a vector space containing P as a hyperplane that does not pass through the origin.

Values of type Homogenization R P can be constructed as linear combinations of Homogenization.ofPoint and Homogenization.ofVector. To define a linear map on Homogenization R P, use Homogenization.lift.

Equations

• Homogenization R P = (V × R)

noncomputable def Homogenization.equivProdAux {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] : Homogenization R P ≃ V × R

Auxiliary definition used for defining the module structure on Homogenization.

Equations

• Homogenization.equivProdAux = Equiv.refl (Homogenization R P)

@[instance_reducible]

noncomputable instance Homogenization.instAddCommGroup {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] : AddCommGroup (Homogenization R P)

Equations

• Homogenization.instAddCommGroup = Homogenization.equivProdAux.addCommGroup

@[instance_reducible]

noncomputable instance Homogenization.instModule {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {S : Type u_11} [Semiring S] [Module S R] [Module S V] [IsScalarTower S R V] : Module S (Homogenization R P)

Equations

• Homogenization.instModule = AddEquiv.module S Homogenization.equivProdAux.addEquiv

instance Homogenization.instIsScalarTower {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {S : Type u_11} [Semiring S] [Module S R] [Module S V] [IsScalarTower S R V] {T : Type u_12} [Semiring T] [Module T R] [Module T V] [IsScalarTower T R V] [SMul S T] [IsScalarTower S T R] [IsScalarTower S T V] : IsScalarTower S T (Homogenization R P)

noncomputable def Homogenization.ofPoint {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] : P →ᵃ[R] Homogenization R P

The embedding of the affine space into the homogenization.

Equations

• Homogenization.ofPoint = (↑(AffineEquiv.vaddConst R (Classical.arbitrary P)).symm).prod (AffineMap.const R P 1)

noncomputable def Homogenization.ofVector {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] : V →ₗ[R] Homogenization R P

The embedding of the vector space into the homogenization.

Equations

• Homogenization.ofVector = Homogenization.ofPoint.linear

@[simp]

theorem Homogenization.ofPoint_linear {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] : ofPoint.linear = ofVector

@[simp]

theorem Homogenization.ofVector_vsub {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] (p q : P) : ofVector (p -ᵥ q) = ofPoint p - ofPoint q

@[simp]

theorem Homogenization.ofVector_smul {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {S : Type u_11} [Semiring S] [Module S R] [Module S V] [IsScalarTower S R V] (c : S) (v : V) : ofVector (c • v) = c • ofVector v

theorem Homogenization.ofVector_injective {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] : Function.Injective ⇑ofVector

theorem Homogenization.ofPoint_injective {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] : Function.Injective ⇑ofPoint

theorem Homogenization.induction_on {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {motive : Homogenization R P → Prop} (x : Homogenization R P) (h : ∀ (v : V) (c : R) (p : P), motive (ofVector v + c • ofPoint p)) : motive x

Every element of the homogenization can be written in the form ofVector v + c • ofPoint p.

See also induction_of_point and ofVector_ofPoint_cases.

theorem Homogenization.induction_of_point {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {motive : Homogenization R P → Prop} (p : P) (x : Homogenization R P) (h : ∀ (v : V) (c : R), motive (ofVector v + c • ofPoint p)) : motive x

Every element of the homogenization can be written in the form ofVector v + c • ofPoint p, where p can be chosen arbitrarily.

theorem Homogenization.ofVector_ofPoint_cases {R : Type u_11} {V : Type u_12} {P : Type u_13} [DivisionRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : Homogenization R P) {motive : Homogenization R P → Prop} (smul_ofPoint : ∀ (c : R) (p : P), c ≠ 0 → motive (c • ofPoint p)) (ofVector : ∀ (v : V), motive (ofVector v)) : motive x

Over a division ring R, every element of Homogenization R P is either a nonzero multiple of a point of P, or an element of the vector space associated to P.

theorem Homogenization.span_range_ofPoint {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] : Submodule.span R (Set.range ⇑ofPoint) = ⊤

theorem Homogenization.hom_ext {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {W : Type u_10} [AddCommGroup W] [Module R W] {f g : Homogenization R P →ₗ[R] W} (h : ∀ (x : P), f (ofPoint x) = g (ofPoint x)) : f = g

theorem Homogenization.hom_ext_iff {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {W : Type u_10} [AddCommGroup W] [Module R W] {f g : Homogenization R P →ₗ[R] W} : f = g ↔ ∀ (x : P), f (ofPoint x) = g (ofPoint x)

noncomputable def Homogenization.lift {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {W : Type u_10} [AddCommGroup W] [Module R W] : (P →ᵃ[R] W) ≃+ (Homogenization R P →ₗ[R] W)

An affine map on P taking values in a vector space extends uniquely to a linear map on Homogenization R P.

See also Homogenization.liftₗ for a version that is linear over some semiring.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Homogenization.lift_apply_ofPoint {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {W : Type u_10} [AddCommGroup W] [Module R W] (f : P →ᵃ[R] W) (p : P) : (lift f) (ofPoint p) = f p

@[simp]

theorem Homogenization.lift_apply_ofVector {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {W : Type u_10} [AddCommGroup W] [Module R W] (f : P →ᵃ[R] W) (v : V) : (lift f) (ofVector v) = f.linear v

@[simp]

theorem Homogenization.lift_symm_apply {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {W : Type u_10} [AddCommGroup W] [Module R W] (f : Homogenization R P →ₗ[R] W) (p : P) : (lift.symm f) p = f (ofPoint p)

@[simp]

theorem Homogenization.lift_symm_linear_apply {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {W : Type u_10} [AddCommGroup W] [Module R W] (f : Homogenization R P →ₗ[R] W) (v : V) : (lift.symm f).linear v = f (ofVector v)

theorem Homogenization.lift_symm_id {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] : lift.symm LinearMap.id = ofPoint

theorem Homogenization.lift_ofPoint {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] : lift ofPoint = LinearMap.id

@[simp]

theorem Homogenization.lift_smul {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {W : Type u_10} [AddCommGroup W] [Module R W] {S : Type u_11} [Semiring S] [Module S W] [SMulCommClass R S W] (c : S) (f : P →ᵃ[R] W) : lift (c • f) = c • lift f

@[simp]

theorem Homogenization.lift_symm_smul {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {W : Type u_10} [AddCommGroup W] [Module R W] {S : Type u_11} [Semiring S] [Module S W] [SMulCommClass R S W] (c : S) (f : Homogenization R P →ₗ[R] W) : lift.symm (c • f) = c • lift.symm f

noncomputable def Homogenization.liftₗ {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {W : Type u_10} [AddCommGroup W] [Module R W] (S : Type u_11) [Semiring S] [Module S W] [SMulCommClass R S W] : (P →ᵃ[R] W) ≃ₗ[S] Homogenization R P →ₗ[R] W

Linear version of Homogenization.lift.

Equations

• Homogenization.liftₗ S = Homogenization.lift.toLinearEquiv ⋯

@[simp]

theorem Homogenization.coe_liftₗ {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {W : Type u_10} [AddCommGroup W] [Module R W] {S : Type u_11} [Semiring S] [Module S W] [SMulCommClass R S W] : ⇑(liftₗ S) = ⇑lift

@[simp]

theorem Homogenization.coe_liftₗ_symm {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {W : Type u_10} [AddCommGroup W] [Module R W] {S : Type u_11} [Semiring S] [Module S W] [SMulCommClass R S W] : ⇑(liftₗ S).symm = ⇑lift.symm

noncomputable def Homogenization.weight {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] : Homogenization R P →ₗ[R] R

The linear map that is constantly 1 when restricted to P.

Equations

• Homogenization.weight = Homogenization.lift (AffineMap.const R P 1)

@[simp]

theorem Homogenization.weight_ofVector {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] (v : V) : weight (ofVector v) = 0

@[simp]

theorem Homogenization.weight_ofPoint {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] (p : P) : weight (ofPoint p) = 1

theorem Homogenization.weight_eq_zero_iff {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {x : Homogenization R P} : weight x = 0 ↔ ∃ (v : V), x = ofVector v

theorem Homogenization.weight_eq_one_iff {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {x : Homogenization R P} : weight x = 1 ↔ ∃ (p : P), x = ofPoint p

theorem Homogenization.lift_const_apply {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {W : Type u_10} [AddCommGroup W] [Module R W] (u : W) (x : Homogenization R P) : (lift (AffineMap.const R P u)) x = weight x • u

theorem Homogenization.weight_surjective {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] : Function.Surjective ⇑weight

noncomputable def Homogenization.map {R : Type u_1} [Ring R] {V₁ : Type u_4} {P₁ : Type u_5} [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁] {V₂ : Type u_6} {P₂ : Type u_7} [AddCommGroup V₂] [Module R V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) : Homogenization R P₁ →ₗ[R] Homogenization R P₂

An affine map between two affine spaces extends to a linear map between their homogenizations.

Equations

• Homogenization.map f = Homogenization.lift (Homogenization.ofPoint.comp f)

@[simp]

theorem Homogenization.map_apply_ofPoint {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {V₁ : Type u_4} {P₁ : Type u_5} [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁] (f : P₁ →ᵃ[R] P) (p : P₁) : (map f) (ofPoint p) = ofPoint (f p)

@[simp]

theorem Homogenization.map_apply_ofVector {R : Type u_1} [Ring R] {V₁ : Type u_4} {P₁ : Type u_5} [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁] {V₂ : Type u_6} {P₂ : Type u_7} [AddCommGroup V₂] [Module R V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) (v : V₁) : (map f) (ofVector v) = ofVector (f.linear v)

@[simp]

theorem Homogenization.map_id {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] : map (AffineMap.id R P) = LinearMap.id

theorem Homogenization.map_injective' {R : Type u_1} [Ring R] {V₁ : Type u_4} {P₁ : Type u_5} [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁] {V₂ : Type u_6} {P₂ : Type u_7} [AddCommGroup V₂] [Module R V₂] [AddTorsor V₂ P₂] : Function.Injective map

@[simp]

theorem Homogenization.map_eq_id_iff {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {f : P →ᵃ[R] P} : map f = LinearMap.id ↔ f = AffineMap.id R P

theorem Homogenization.map_comp {R : Type u_1} [Ring R] {V₁ : Type u_4} {P₁ : Type u_5} [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁] {V₂ : Type u_6} {P₂ : Type u_7} [AddCommGroup V₂] [Module R V₂] [AddTorsor V₂ P₂] {V₃ : Type u_8} {P₃ : Type u_9} [AddCommGroup V₃] [Module R V₃] [AddTorsor V₃ P₃] (f : P₂ →ᵃ[R] P₃) (g : P₁ →ᵃ[R] P₂) : map (f.comp g) = map f ∘ₗ map g

@[simp]

theorem Homogenization.weight_map {R : Type u_1} [Ring R] {V₁ : Type u_4} {P₁ : Type u_5} [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁] {V₂ : Type u_6} {P₂ : Type u_7} [AddCommGroup V₂] [Module R V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[R] P₂) (x : Homogenization R P₁) : weight ((map f) x) = weight x

theorem Homogenization.lift_map {R : Type u_1} [Ring R] {V₁ : Type u_4} {P₁ : Type u_5} [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁] {V₂ : Type u_6} {P₂ : Type u_7} [AddCommGroup V₂] [Module R V₂] [AddTorsor V₂ P₂] {V₃ : Type u_8} [AddCommGroup V₃] [Module R V₃] (f : P₂ →ᵃ[R] V₃) (g : P₁ →ᵃ[R] P₂) (x : Homogenization R P₁) : (lift f) ((map g) x) = (lift (f.comp g)) x

@[simp]

theorem Homogenization.map_injective {R : Type u_1} [Ring R] {V₁ : Type u_4} {P₁ : Type u_5} [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁] {V₂ : Type u_6} {P₂ : Type u_7} [AddCommGroup V₂] [Module R V₂] [AddTorsor V₂ P₂] {f : P₁ →ᵃ[R] P₂} : Function.Injective ⇑(map f) ↔ Function.Injective ⇑f

@[simp]

theorem Homogenization.map_surjective {R : Type u_1} [Ring R] {V₁ : Type u_4} {P₁ : Type u_5} [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁] {V₂ : Type u_6} {P₂ : Type u_7} [AddCommGroup V₂] [Module R V₂] [AddTorsor V₂ P₂] {f : P₁ →ᵃ[R] P₂} : Function.Surjective ⇑(map f) ↔ Function.Surjective ⇑f

noncomputable def Homogenization.congr {R : Type u_1} [Ring R] {V₁ : Type u_4} {P₁ : Type u_5} [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁] {V₂ : Type u_6} {P₂ : Type u_7} [AddCommGroup V₂] [Module R V₂] [AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[R] P₂) : Homogenization R P₁ ≃ₗ[R] Homogenization R P₂

An affine isomorphism between two affine spaces extends to a linear isomorphism between their homogenizations.

Equations

• Homogenization.congr f = LinearEquiv.ofLinearMap (Homogenization.map ↑f) (Homogenization.map ↑f.symm) ⋯ ⋯

@[simp]

theorem Homogenization.coe_congr {R : Type u_1} [Ring R] {V₁ : Type u_4} {P₁ : Type u_5} [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁] {V₂ : Type u_6} {P₂ : Type u_7} [AddCommGroup V₂] [Module R V₂] [AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[R] P₂) : ⇑(congr f) = ⇑(map ↑f)

@[simp]

theorem Homogenization.toLinearMap_congr {R : Type u_1} [Ring R] {V₁ : Type u_4} {P₁ : Type u_5} [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁] {V₂ : Type u_6} {P₂ : Type u_7} [AddCommGroup V₂] [Module R V₂] [AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[R] P₂) : ↑(congr f) = map ↑f

@[simp]

theorem Homogenization.congr_symm {R : Type u_1} [Ring R] {V₁ : Type u_4} {P₁ : Type u_5} [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁] {V₂ : Type u_6} {P₂ : Type u_7} [AddCommGroup V₂] [Module R V₂] [AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[R] P₂) : (congr f).symm = congr f.symm

@[simp]

theorem Homogenization.congr_refl {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] : congr (AffineEquiv.refl R P) = LinearEquiv.refl R (Homogenization R P)

@[simp]

theorem Homogenization.congr_eq_refl_iff {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] {f : P ≃ᵃ[R] P} : congr f = LinearEquiv.refl R (Homogenization R P) ↔ f = AffineEquiv.refl R P

theorem Homogenization.congr_trans {R : Type u_1} [Ring R] {V₁ : Type u_4} {P₁ : Type u_5} [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁] {V₂ : Type u_6} {P₂ : Type u_7} [AddCommGroup V₂] [Module R V₂] [AddTorsor V₂ P₂] {V₃ : Type u_8} {P₃ : Type u_9} [AddCommGroup V₃] [Module R V₃] [AddTorsor V₃ P₃] (f : P₁ ≃ᵃ[R] P₂) (g : P₂ ≃ᵃ[R] P₃) : congr (f.trans g) = congr f ≪≫ₗ congr g

noncomputable def Homogenization.toProd {R : Type u_1} [Ring R] {V : Type u_2} [AddCommGroup V] [Module R V] : Homogenization R V ≃ₗ[R] V × R

The homogenization of a vector space V over R is canonically isomorphic to V × R

Equations

• One or more equations did not get rendered due to their size.

theorem Homogenization.toProd_symm_apply {R : Type u_1} [Ring R] {V : Type u_2} [AddCommGroup V] [Module R V] (x : V × R) : toProd.symm x = ofVector x.1 + x.2 • ofPoint 0

theorem Homogenization.toProd_apply {R : Type u_1} [Ring R] {V : Type u_2} [AddCommGroup V] [Module R V] (i : Homogenization R V) : toProd i = ((lift (AffineMap.id R V)) i, weight i)

@[simp]

theorem Homogenization.toProd_ofPoint {R : Type u_1} [Ring R] {V : Type u_2} [AddCommGroup V] [Module R V] (v : V) : toProd (ofPoint v) = (v, 1)

@[simp]

theorem Homogenization.toProd_ofVector {R : Type u_1} [Ring R] {V : Type u_2} [AddCommGroup V] [Module R V] (v : V) : toProd (ofVector v) = (v, 0)

instance Homogenization.instFinite {R : Type u_1} [Ring R] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module R V] [AddTorsor V P] [Module.Finite R V] : Module.Finite R (Homogenization R P)