Projectivization.Subspace.span_univ
theorem Projectivization.Subspace.span_univ :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
Projectivization.Subspace.span Set.univ = ⊤
This theorem states that the span of the entire projective space is the greatest (top) element in the lattice of subspaces. In more detail, for any field `K` and any additive commutative group `V` that is also a `K`-module, when you take the span (i.e., the smallest subspace that includes a given set of vectors) of the set of all points in the projective space (the universal set), you end up with the entire projective space itself, symbolized by `⊤`. This is akin to saying that every vector in the projective space can be expressed as a linear combination of vectors from the entire projective space.
More concisely: The span of all points in a projective space over a field forms the greatest subspace in the lattice of subspaces.
|
Projectivization.Subspace.span_empty
theorem Projectivization.Subspace.span_empty :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
Projectivization.Subspace.span ∅ = ⊥
This theorem states that for any field `K` and any additive commutative group `V` that is also a `K`-module, the span of the empty set in the projective space over `K` and `V`, as defined by `Projectivization.Subspace.span`, is equal to the bottom element `⊥` of the lattice of subspaces. This means that the smallest subspace that includes no points is the trivial subspace.
More concisely: The span of the empty set in the projective space over a field `K` and an additive commutative `K`-module `V` is the trivial subspace.
|
Projectivization.Subspace.sup_span
theorem Projectivization.Subspace.sup_span :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
{S : Set (Projectivization K V)} {W : Projectivization.Subspace K V},
W ⊔ Projectivization.Subspace.span S = Projectivization.Subspace.span (↑W ∪ S)
This theorem states that for any field `K`, an additive commutative group `V`, and any `K`-module `V`, the supremum (join in the lattice of subspaces) of a subspace `W` of the projectivized `K`-vector space `V` and the subspace spanned by a set of points `S` in the projectivized `K`-vector space `V`, is equal to the subspace spanned by the union of the subspace `W` and the set `S`. In other words, adding new points to a subspace and then taking the span is the same as first taking the span of the new points and then taking the supremum with the original subspace.
More concisely: For any field `K`, additive commutative group `V`, `K`-module `V`, subspace `W` of the projectivized `K`-vector space `V`, and set `S` of points in `V`, the supremum of `W` and the subspace spanned by `S` in the lattice of subspaces equals the subspace spanned by the union of `W` and `S`.
|
Projectivization.Subspace.span_iUnion
theorem Projectivization.Subspace.span_iUnion :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Sort u_3}
(s : ι → Set (Projectivization K V)),
Projectivization.Subspace.span (⋃ i, s i) = ⨆ i, Projectivization.Subspace.span (s i)
This theorem states that for any index set ι and a family of sets in the projectivization of a K-vector space V (where K is a field and V is an additive commutative group with a K-module structure), the span of the union of these sets is equal to the supremum of the spans of each individual set. In simpler terms, if you have a collection of subspaces in a projective space, the largest subspace that contains all of these subspaces (the supremum) is the same as the subspace you get by taking all the points in these subspaces together and then taking the span.
More concisely: Given a family of subspaces in the projective space of a K-vector space V, the span of their union equals the supremum of their individual spans.
|
Projectivization.Subspace.span_union
theorem Projectivization.Subspace.span_union :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
(S T : Set (Projectivization K V)),
Projectivization.Subspace.span (S ∪ T) = Projectivization.Subspace.span S ⊔ Projectivization.Subspace.span T
This theorem states that in a projective space, which is built over a vector space 'V' on a field 'K', the supremum of two subspaces is equal to the span of their union. Here, the span of a set of points in the projective space is itself a subspace. For any two sets 'S' and 'T' of elements in the projective space, the span of the union of 'S' and 'T' is the same as the supremum of the spans of 'S' and 'T' individually. In mathematical terms, the theorem is expressing the fact that `span(S ∪ T) = span(S) ⊔ span(T)`, where 'span' denotes the span operation, '∪' denotes set union, and '⊔' denotes the supremum operation.
More concisely: In a projective space over a field, the span of the union of two subspaces equals the supremum of their individual spans.
|
Projectivization.Subspace.mem_add
theorem Projectivization.Subspace.mem_add :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
(T : Projectivization.Subspace K V) (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
Projectivization.mk K v hv ∈ T → Projectivization.mk K w hw ∈ T → Projectivization.mk K (v + w) hvw ∈ T
The theorem `Projectivization.Subspace.mem_add` states that for any field `K`, vector space `V` over `K`, a subspace `T` of the projectivization of `V`, and non-zero vectors `v`, `w` in `V` such that their sum `v + w` is also non-zero, if the projectivization of `v` is in `T` and the projectivization of `w` is in `T`, then the projectivization of `v + w` is also in `T`. In other words, this theorem asserts that the subspace `T` of the projectivization of a vector space is closed under addition.
More concisely: Given a field `K`, a vector space `V` over `K`, a subspace `T` of the projectivization of `V`, and non-zero vectors `v`, `w` in `V` such that `v + w` is non-zero, if the projectivizations of `v` and `w` belong to `T`, then the projectivization of `v + w` also belongs to `T`.
|
Projectivization.Subspace.monotone_span
theorem Projectivization.Subspace.monotone_span :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
Monotone Projectivization.Subspace.span
This theorem states that for any field `K` and any additive commutative group `V` that also has a structure of `K`-module, the span function in the projective space is monotone. In other words, if a set of points is a subset of another set of points in the projective space, then the span of the subset (the smallest subspace containing all the points in the subset) will be contained in, or equal to, the span of the larger set.
More concisely: Given a field `K`, an additive commutative group `V` with a `K`-module structure, the span of a subset of points in the projective space of `V` is contained in, or equal to, the span of any larger subset of points.
|
Projectivization.Subspace.subset_span
theorem Projectivization.Subspace.subset_span :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
(S : Set (Projectivization K V)), S ⊆ ↑(Projectivization.Subspace.span S)
This theorem states that for any field `K`, and a given additively commutative group `V` which is also a module over `K`, the span (defined in projective space) of a set `S` of points in the projectivization of the vector space `V` over `K` always contains the original set `S`. In other words, every point in `S` is also a point in the span of `S`.
More concisely: For any field `K` and additively commutative `K`-module `V`, the projective span of a set `S` of points in the projectivization of `V` contains `S`.
|
Projectivization.Subspace.span_eq_span_iff
theorem Projectivization.Subspace.span_eq_span_iff :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
{S T : Set (Projectivization K V)},
Projectivization.Subspace.span S = Projectivization.Subspace.span T ↔
S ⊆ ↑(Projectivization.Subspace.span T) ∧ T ⊆ ↑(Projectivization.Subspace.span S)
This theorem states that for any two sets of points `S` and `T` in a projective space, the span of `S` is equal to the span of `T` if and only if each set of points is contained in the span of the other set. Here, the projective space is defined over a field `K` and a vector space `V` with a given addition group and module structure. The symbol `⊆` represents the subset relation, meaning all elements of the first set are also elements of the second set. The notation `↑` is used to denote a coercion or type conversion, in this case, converting a subspace to a set.
More concisely: For sets of points S and T in a projective space over field K, their spans are equal if and only if each set is contained in the span of the other. (Equivalently, the subspaces spanned by S and T are equal.)
|
Projectivization.Subspace.span_coe
theorem Projectivization.Subspace.span_coe :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
(W : Projectivization.Subspace K V), Projectivization.Subspace.span ↑W = W
This theorem states that for any given subspace of a projective space, the span of this subspace is the subspace itself. Here, the projective space is defined over a field `K` and a commutative additive group `V` that also forms a module over `K`. In other words, spanning doesn't change a subspace in the context of projective geometry.
More concisely: In projective geometry over a field `K`, the span of a subspace is equal to the subspace itself.
|
Projectivization.Subspace.span_eq_sInf
theorem Projectivization.Subspace.span_eq_sInf :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
{S : Set (Projectivization K V)}, Projectivization.Subspace.span S = sInf {W | S ⊆ ↑W}
The theorem `Projectivization.Subspace.span_eq_sInf` states that for any field `K`, any additive commutative group `V`, any module `V` over `K`, and any set `S` of points in the projective space `ℙ K V`, the span of the set `S` is equal to the infimum of the collection of subspaces `W` such that `S` is a subset of `W`. In other words, the smallest subspace that contains all points in `S` is exactly the span of `S`. The infimum here is taken with respect to the inclusion order of subspaces.
More concisely: The smallest subspace containing a set of points in projective space is equal to their span.
|
Projectivization.Subspace.mem_span
theorem Projectivization.Subspace.mem_span :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
{S : Set (Projectivization K V)} (u : Projectivization K V),
u ∈ Projectivization.Subspace.span S ↔ ∀ (W : Projectivization.Subspace K V), S ⊆ ↑W → u ∈ W
This theorem states that for any given field `K` and an additive commutative group `V` over which `K` is a module, a point `u` is contained in the span of a set `S` in the projective space over `K` and `V` if and only if the point `u` is contained in all subspaces `W` of the projective space that contain the set `S`. Here, the span of a set of points is the smallest subspace that contains all the points in the set. In essence, the theorem provides a characterization of membership in the span in terms of containment in all larger subspaces.
More concisely: A point `u` in the projective space over a field `K` and additive commutative group `V` is contained in the span of a set `S` if and only if it belongs to every subspace of the projective space containing `S`.
|
Projectivization.Subspace.span_eq_of_le
theorem Projectivization.Subspace.span_eq_of_le :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
{S : Set (Projectivization K V)} {W : Projectivization.Subspace K V},
S ⊆ ↑W → W ≤ Projectivization.Subspace.span S → Projectivization.Subspace.span S = W
This theorem states that for any field `K`, additive commutative group `V`, and a module over `K` and `V`, if you have a set of points `S` in the projectivized space of `K` and `V`, and a subspace `W` of that projectivized space, then if `S` is contained in `W` and `W` is contained in the span of `S`, then the span of `S` is precisely equal to `W`. In other words, the span of a set of points is the smallest subspace containing those points. This is a fundamental concept in linear algebra, where the span of a set of vectors in a vector space forms a subspace of that vector space.
More concisely: Given a field `K`, an additive commutative group `V`, a module over `K` and `V`, a set `S` of points in the projectivized space of `K` and `V`, and a subspace `W` of that projectivized space containing `S`, if `S` is contained in the span of `W` and `W` is contained in the span of `S`, then the span of `S` equals `W`.
|
Projectivization.Subspace.span_le_subspace_iff
theorem Projectivization.Subspace.span_le_subspace_iff :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
{S : Set (Projectivization K V)} {W : Projectivization.Subspace K V},
Projectivization.Subspace.span S ≤ W ↔ S ⊆ ↑W
The theorem `Projectivization.Subspace.span_le_subspace_iff` states that for any field `K`, an additive commutative group `V`, and any module structure on `V` over `K`, and for any set `S` of points in the projectivization of the `K`-vector space `V` and any subspace `W` of this projectivization, the span of the set `S` is contained in the subspace `W` if and only if the all the points in set `S` are contained in the subspace `W`. In other words, the span of a set of points is a subspace of another specific subspace if and only if every single point in the original set is an element of that specific subspace.
More concisely: For any projective space over a field, a set of points spans a subspace if and only if every point in the set is contained in the subspace.
|
Projectivization.Subspace.mem_add'
theorem Projectivization.Subspace.mem_add' :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
(self : Projectivization.Subspace K V) (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
Projectivization.mk K v hv ∈ self.carrier →
Projectivization.mk K w hw ∈ self.carrier → Projectivization.mk K (v + w) hvw ∈ self.carrier
The theorem `Projectivization.Subspace.mem_add'` states that for any division ring `K`, a vector space `V` over `K`, a subspace of the projectivization of `V` (denoted as `self`), and any two nonzero vectors `v` and `w` in `V` such that their sum is also nonzero, if `v` and `w` are elements of the carrier of the subspace when considered as elements of the projectivization, then their sum is also an element of the carrier of that subspace. In other words, the theorem asserts that the addition of two vectors in a projective subspace results in another vector in the same projective subspace.
More concisely: Given a division ring K, a vector space V over K, a subspace of the projectivization of V, and two nonzero vectors v and w in V with their sum being nonzero, if v and w are in the subspace, then their sum is also in the subspace.
|