Normalized representatives of projective points

A projective point represented by a tuple can be normalized at any nonzero coordinate. The resulting representative has that coordinate equal to 1, and its other coordinates are the corresponding ratios. This gives affine coordinates without a finiteness assumption on the index type.

The file also describes the fibres of Projectivization.mk' as orbits of the units of the scalar ring: two nonzero vectors give the same point exactly when one is a unit multiple of the other (Projectivization.mk'_eq_mk'_iff), so the saturation of a set of nonzero vectors is the union of its unit translates (Projectivization.preimage_image_mk'). These two lemmas are from Zayn Blore's Mathlib pull request mathlib4#44117. Equivalently, two nonzero vectors give the same point exactly when the first lies on the line spanned by the second (Projectivization.mk_eq_mk_iff_mem_span).

A linear map G : V →ₗ[K] W induces the map Projectivization.linearProjection G, sending [v] to [G v] on the set Projectivization.linearProjectionDomain G of points where G does not vanish (Projectivization.linearProjection_mk).

The projectivization of a vector space of dimension at most one, such as Projectivization K (Fin 1 → K), has at most one point (Projectivization.subsingleton_of_rank_le_one).

The file also records Projectivization.submodule_map: the line of the image of a projective point under an injective semilinear map is the image of its line.

The normalization lemmas are adapted from Ralf Stephan's ArithmeticHeights/Northcott.lean in rwst/Subspace-Theorems, commit e443c2479e19f7665b31d8e94e2317c8ced1ca06 (Apache 2.0).

@[simp]

theorem Projectivization.coe_equivSubmodule (K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (p : Projectivization K V) : ↑((equivSubmodule K V) p) = p.submodule

The equivalence with one-dimensional subspaces retains the underlying line.

theorem Projectivization.mk_eq_mk_iff_mem_span {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {v w : V} (hv : v ≠ 0) (hw : w ≠ 0) : mk K v hv = mk K w hw ↔ v ∈ K ∙ w

Two nonzero vectors give the same projective point exactly when the first lies on the line spanned by the second.

theorem Projectivization.subsingleton_of_rank_le_one {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (h : Module.rank K V ≤ 1) : Subsingleton (Projectivization K V)

The projectivization of a vector space of dimension at most one has at most one point: all nonzero vectors of a line span the same line.

def Projectivization.linearProjectionDomain {K : Type u_1} {V : Type u_2} {W : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] (G : V →ₗ[K] W) : Set (Projectivization K V)

The points [v] of ℙ K V with G v ≠ 0, for a linear map G : V →ₗ[K] W: the complement of the projectivized kernel of G, on which G induces the map Projectivization.linearProjection G.

@[simp]

theorem Projectivization.mk_mem_linearProjectionDomain_iff {K : Type u_1} {V : Type u_2} {W : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] (G : V →ₗ[K] W) {v : V} (hv : v ≠ 0) : mk K v hv ∈ linearProjectionDomain G ↔ G v ≠ 0

The point [v] lies in the domain of Projectivization.linearProjection G iff G v ≠ 0.

theorem Projectivization.mem_linearProjectionDomain_iff {K : Type u_1} {V : Type u_2} {W : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] (G : V →ₗ[K] W) {y : Projectivization K V} : y ∈ linearProjectionDomain G ↔ G y.rep ≠ 0

A point lies in the domain of Projectivization.linearProjection G iff G does not vanish on its representative.

noncomputable def Projectivization.linearProjection {K : Type u_1} {V : Type u_2} {W : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [Nonempty (Projectivization K W)] (G : V →ₗ[K] W) : Projectivization K V → Projectivization K W

The map [v] ↦ [G v] of projective spaces induced by a linear map G, on the set Projectivization.linearProjectionDomain G of points where G does not vanish; it sends the projectivized kernel of G to an arbitrary point. For surjective G it is the projection from the projectivized kernel.

@[simp]

theorem Projectivization.linearProjection_mk {K : Type u_1} {V : Type u_2} {W : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [Nonempty (Projectivization K W)] (G : V →ₗ[K] W) {v : V} (hv : v ≠ 0) (h : G v ≠ 0) : linearProjection G (mk K v hv) = mk K (G v) h

The map induced by a linear map G in homogeneous coordinates, where G does not vanish.

theorem Projectivization.exists_rep_apply_eq_one_of_ne_zero {K : Type u_1} [Field K] {ι : Type u_2} (x : Projectivization K (ι → K)) {i : ι} (hi : x.rep i ≠ 0) : ∃ (v : ι → K) (hv : v ≠ 0), v i = 1 ∧ (∀ (j : ι), v j = x.rep j / x.rep i) ∧ mk K v hv = x

At any nonzero coordinate of a projective point, there is a representative normalized to 1 whose coordinates are the ratios of the chosen representative's coordinates.

theorem Projectivization.exists_rep_apply_eq_one {K : Type u_1} [Field K] {ι : Type u_2} (x : Projectivization K (ι → K)) : ∃ (v : ι → K) (hv : v ≠ 0) (i : ι), v i = 1 ∧ (∀ (j : ι), v j = x.rep j / x.rep i) ∧ mk K v hv = x

Every projective point has a representative with some coordinate equal to 1, and its coordinates are the ratios at that coordinate.

@[simp]

theorem Projectivization.submodule_map {D : Type u_3} {E : Type u_4} {V : Type u_5} {W : Type u_6} [DivisionRing D] [DivisionRing E] [AddCommGroup V] [Module D V] [AddCommGroup W] [Module E W] {σ : D →+* E} [RingHomSurjective σ] (f : V →ₛₗ[σ] W) (hf : Function.Injective ⇑f) (x : Projectivization D V) : (map f hf x).submodule = Submodule.map f x.submodule

The line of the image of a projective point under an injective semilinear map is the image of its line.