Projectivization.mk_eq_mk_iff
theorem Projectivization.mk_eq_mk_iff :
∀ (K : Type u_1) {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (v w : V)
(hv : v ≠ 0) (hw : w ≠ 0), Projectivization.mk K v hv = Projectivization.mk K w hw ↔ ∃ a, a • w = v
This theorem states that for any division ring `K` and additive commutative group `V` that is also a `K`-module, and any two non-zero vectors `v` and `w` in `V`, the projective coordinates of `v` and `w` (constructed using `Projectivization.mk`) are equal if and only if there exists a scalar `a` from the ring `K` such that `v` is a scalar multiple of `w`, that is `v` equals `a` scaled by `w`, denoted as `a • w = v` in mathematical notation. This theorem essentially captures the idea of equivalence in projective coordinates, where two non-zero vectors are considered equivalent if they are scalar multiples of each other.
More concisely: For any division ring `K`, additive commutative group `V` being a `K`-module, and non-zero vectors `v` and `w` in `V`, the projective coordinates of `v` and `w` are equal if and only if there exists `a` in `K` such that `v = a • w`.
|
Projectivization.map_injective
theorem Projectivization.map_injective :
∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
{L : Type u_3} {W : Type u_4} [inst_3 : DivisionRing L] [inst_4 : AddCommGroup W] [inst_5 : Module L W]
{σ : K →+* L} {τ : L →+* K} [inst_6 : RingHomInvPair σ τ] (f : V →ₛₗ[σ] W) (hf : Function.Injective ⇑f),
Function.Injective (Projectivization.map f hf)
The theorem `Projectivization.map_injective` states that for any semilinear map `f : V →ₛₗ[σ] W` over an isomorphism of fields `σ : K →+* L` and `τ : L →+* K`, where `K` and `L` are division rings, `V` and `W` are additive commutative groups, and `V` and `W` are modules over `K` and `L` respectively, if the semilinear map `f` is injective, then the corresponding map on projective spaces defined by `f`, namely `Projectivization.map f hf`, is also injective. Here, injectivity means that if two elements map to the same value, they were the same to begin with. In other words, no information is lost in the mapping process.
More concisely: If `f : V →ₛₗ[σ] W` is an injective semilinear map between `K`-module `V` and `L`-module `W` over isomorphisms `σ : K →+* L` and `τ : L →+* K`, then the induced map on projective spaces `Projectivization.map f` is also injective.
|
Projectivization.ind
theorem Projectivization.ind :
∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
{P : Projectivization K V → Prop},
(∀ (v : V) (h : v ≠ 0), P (Projectivization.mk K v h)) → ∀ (p : Projectivization K V), P p
This theorem is an induction principle for the concept of Projectivization. It states that for any given division ring `K`, additive commutative group `V`, and a `K`-module structure on `V`, if a property `P` holds for all elements of the projectivization of `V` over `K` that are constructed from non-zero vectors in `V` using the `Projectivization.mk` constructor, then this property `P` holds for all elements of the projectivization of `V` over `K`.
In other words, you can prove a property about all points in the projective space by proving it for all non-zero vectors in the vector space, utilizing the `Projectivization.mk` function to relate the vector space and the projective space.
More concisely: If a property holds for all projective points in the projectivization of a `K`-module `V` constructed from non-zero vectors, then it holds for all projective points in the projectivization of `V` over the division ring `K`.
|
Projectivization.mk_rep
theorem Projectivization.mk_rep :
∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
(v : Projectivization K V), Projectivization.mk K v.rep ⋯ = v
The theorem `Projectivization.mk_rep` states that for any projectivized vector `v` (from the projectivization of a vector space `V` over a division ring `K`), if we take a representative of `v` in `V` using the `Projectivization.rep` function, and then project it back into the projectivization using `Projectivization.mk`, we get the original projectivized vector `v` back. This theorem essentially says that the process of projecting a vector into the projectivization and then retrieving a representative from the projectivization is idempotent.
More concisely: For any projectivized vector `v` from the projectivization of a vector space `V` over a division ring `K`, `Projectivization.mk (Projectivization.rep v) = v`.
|
Projectivization.rep_nonzero
theorem Projectivization.rep_nonzero :
∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
(v : Projectivization K V), v.rep ≠ 0
The theorem `Projectivization.rep_nonzero` states that for any division ring `K` and any additive commutative group `V` that is also a `K`-module, the representative of any element `v` of the projectivization of `V` over `K` (obtained using the `Projectivization.rep` function) is always non-zero. In other words, any point in the projective space corresponds to a non-zero vector in the original vector space `V`.
More concisely: For any division ring `K` and additive commutative `K`-module `V`, the representation of any point in the projective space of `V` over `K` is a non-zero vector.
|
Projectivization.mk_eq_mk_iff'
theorem Projectivization.mk_eq_mk_iff' :
∀ (K : Type u_1) {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (v w : V)
(hv : v ≠ 0) (hw : w ≠ 0), Projectivization.mk K v hv = Projectivization.mk K w hw ↔ ∃ a, a • w = v
The theorem `Projectivization.mk_eq_mk_iff'` asserts that for any division ring `K` and any module `V` over `K`, two nonzero vectors `v` and `w` from `V` map to the same point in the projective space constructed from `V` if and only if there exists a scalar `a` from `K` such that `v` is a scalar multiple of `w`, i.e., `a • w = v`. This theorem essentially characterizes the identification of vectors in the projective space: two vectors are identified if they are scalar multiples of each other.
More concisely: Two non-zero vectors in a module over a division ring map to the same point in the projective space if and only if one is a scalar multiple of the other.
|