Projectivization.independent_iff_not_dependent
theorem Projectivization.independent_iff_not_dependent :
∀ {ι : Type u_1} {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V]
[inst_2 : Module K V] {f : ι → Projectivization K V},
Projectivization.Independent f ↔ ¬Projectivization.Dependent f
This theorem states that for any index type `ι`, any division ring `K`, and any abelian (or commutative) additive group `V` that is also a module over `K`, and any function `f` from `ι` to the projectivization of `V` over `K`, the statement "`f` is independent" is equivalent to the negation of the statement "`f` is dependent". In other words, in the projectivization of `V` over `K`, a collection of elements (as indexed by `ι` and given by `f`) is independent if and only if it is not dependent.
More concisely: In the projectivization of an abelian group `V` over a division ring `K`, a function `f : ι -> PV` defines an independent collection of points if and only if it does not define a dependent collection.
|
Projectivization.independent_pair_iff_neq
theorem Projectivization.independent_pair_iff_neq :
∀ {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
(u v : Projectivization K V), Projectivization.Independent ![u, v] ↔ u ≠ v
This theorem states that for any division ring `K`, and any additive commutative group `V` that is also a `K`-module, a pair of points `u` and `v` in the projective space (`Projectivization K V`) is independent if and only if these points `u` and `v` are not equal. Here, the projective space (`Projectivization K V`) is defined as the set of equivalence classes of the `K`-vector space `V`, where two vectors are equivalent if they are scalar multiples of each other.
More concisely: In the projective space over a division ring `K` with respect to a `K`-module `V`, two points represent distinct equivalence classes if and only if they are not equal.
|
Projectivization.independent_iff_completeLattice_independent
theorem Projectivization.independent_iff_completeLattice_independent :
∀ {ι : Type u_1} {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V]
[inst_2 : Module K V] {f : ι → Projectivization K V},
Projectivization.Independent f ↔ CompleteLattice.Independent fun i => (f i).submodule
This theorem states that a family of points in the projective space (projectivization of a `K`-vector space `V`) is independent if and only if the family of submodules determined by these points is independent in the sense of lattice theory. Here, `ι` is a type which indexes the family, `K` is the division ring over which the vector space and projective space are defined, and `V` is the vector space. The `Projectivization.Independent f` represents the independence of the family of points in projective space indexed by `ι`, and `CompleteLattice.Independent fun i => (f i).submodule` represents the independence of the corresponding submodules in the lattice-theoretic sense.
More concisely: A family of points in the projective space of a K-vector space is independent if and only if the submodules determined by these points are independent in the lattice-theoretic sense.
|
Projectivization.independent_iff
theorem Projectivization.independent_iff :
∀ {ι : Type u_1} {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V]
[inst_2 : Module K V] {f : ι → Projectivization K V},
Projectivization.Independent f ↔ LinearIndependent K (Projectivization.rep ∘ f)
The theorem states that a set of points in a projective space, represented by a family `f` mapping from an index set `ι` to the projective space `ℙ K V` (projectivization of the vector space `V` over the division ring `K`), is independent if and only if the representative vectors corresponding to these points are linearly independent. Here, the representative vectors are determined by applying the representative function `Projectivization.rep` to the family `f`. In other words, the projective independence of a set of points is equivalent to the linear independence of their representative vectors in the associated vector space.
More concisely: A set of points in a projective space is independent if and only if the representative vectors of these points are linearly independent in the associated vector space.
|
Projectivization.dependent_iff_not_independent
theorem Projectivization.dependent_iff_not_independent :
∀ {ι : Type u_1} {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V]
[inst_2 : Module K V] {f : ι → Projectivization K V},
Projectivization.Dependent f ↔ ¬Projectivization.Independent f
The theorem `Projectivization.dependent_iff_not_independent` states that for any index type `ι`, any type `K` with a division ring structure, and any type `V` with an additive commutative group structure and a `K`-module structure, a function `f` from `ι` to the projectivization of `K` and `V` is dependent if and only if it is not independent. This theorem essentially captures the mathematical concept that dependence is the negation of independence within the context of projective spaces.
More concisely: For any index type `ι`, function `f` from `ι` to the projectivization of a type `K` with a division ring structure and `V` with an additive commutative group and a `K`-module structure, `f` is dependent if and only if it is not independent.
|
Projectivization.dependent_iff
theorem Projectivization.dependent_iff :
∀ {ι : Type u_1} {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V]
[inst_2 : Module K V] {f : ι → Projectivization K V},
Projectivization.Dependent f ↔ ¬LinearIndependent K (Projectivization.rep ∘ f)
This theorem states that a family of points in a projective space is dependent if and only if their representatives are linearly dependent. The theorem is denoted by `Projectivization.dependent_iff`. In this theorem, `ι` is a type variable representing the indexing set for the family of points, `K` is the field over which the vectors are defined, and `V` is the vector space. The theorem takes as input a function `f` that maps indices to points in the projective space. The theorem states that `f` defines a dependent set in the projective space if and only if the function obtained by composing `f` with the representative picking function `Projectivization.rep` is not a linearly independent function over `K`. This means that the vectors represented by the function `f` are linearly dependent in the vector space `V`.
More concisely: A family of points in projective space is dependent if and only if their representative vectors in the underlying vector space are linearly dependent.
|
Projectivization.dependent_pair_iff_eq
theorem Projectivization.dependent_pair_iff_eq :
∀ {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
(u v : Projectivization K V), Projectivization.Dependent ![u, v] ↔ u = v
This theorem states that for any division ring `K` and an additive commutative group `V` that is also a `K`-module, two points `u` and `v` in the projective space (or the projectivization of the `K`-vector space `V`) are dependent if and only if they are identical. In other words, within the projective space constructed from the `K`-vector space `V`, a pair of points is linearly dependent precisely when they are the same point.
More concisely: In the projective space of a division ring `K`-module `V`, two points are dependent if and only if they are identical.
|