LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingLeft
theorem LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingLeft :
∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {n : Type u_19} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] [inst_3 : AddCommGroup M₁] [inst_4 : Module R M₁] {I I' : R →+* R} [inst_5 : Nontrivial R]
{B : M →ₛₗ[I] M →ₛₗ[I'] M₁} {v : Basis n R M},
B.IsOrthoᵢ ⇑v → B.SeparatingLeft → ∀ (i : n), ¬B.IsOrtho (v i) (v i)
This theorem states that if we have an orthogonal basis relative to a left-separating bilinear map, there are no elements in the basis that are self-orthogonal. Here, the map and the basis are over a module (a generalization of vector spaces) with coefficients in a commutative ring. The theorem applies to any element of the basis, stipulating that the bilinear map cannot return zero when applied to the same basis element twice.
More concisely: In a module with coefficients in a commutative ring, if a basis is orthogonal relative to a left-separating bilinear map, then no basis element is self-orthogonal.
|
LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingRight
theorem LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingRight :
∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {n : Type u_19} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] [inst_3 : AddCommGroup M₁] [inst_4 : Module R M₁] {I I' : R →+* R} [inst_5 : Nontrivial R]
{B : M →ₛₗ[I] M →ₛₗ[I'] M₁} {v : Basis n R M},
B.IsOrthoᵢ ⇑v → B.SeparatingRight → ∀ (i : n), ¬B.IsOrtho (v i) (v i)
This theorem states that for any orthogonal basis with respect to a right-separating bilinear map, none of its elements are self-orthogonal. More specifically, given a commutative ring `R`, two additive commutative groups `M` and `M₁` which are also modules over `R`, two ring homomorphisms `I` and `I'`, a nontrivial instance of `R`, a right-separating bilinear map `B` from `M` to `M₁` and a basis `v` of `M` over `R`, if the basis `v` is orthogonal with respect to the bilinear map `B`, then for every element `i` of the basis `v`, `B` does not yield zero when applied to `v i` and `v i`. This implies that no element of the basis is orthogonal to itself under the bilinear map `B`.
More concisely: Given a right-separating bilinear map B and an orthogonal basis v over R, no element in v is self-orthogonal with respect to B.
|
LinearMap.IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self
theorem LinearMap.IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self :
∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {n : Type u_19} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] [inst_3 : AddCommGroup M₁] [inst_4 : Module R M₁] [inst_5 : NoZeroSMulDivisors R M₁]
{B : M →ₗ[R] M →ₗ[R] M₁} (v : Basis n R M),
B.IsOrthoᵢ ⇑v → (∀ (i : n), ¬B.IsOrtho (v i) (v i)) → B.SeparatingLeft
This theorem states that for any commutative ring `R`, and any modules `M` and `M1` over `R` with a basis `v` for `M`, if `B` is a bilinear map from `M` to `M1` that's orthogonal with respect to `v` and there exists no element in the basis that's self-orthogonal with respect to `B`, then `B` is left-separating. Here, "self-orthogonal" means that applying the bilinear map `B` to an element and itself results in zero. A map is "left-separating" if for any non-zero element of `M`, there is another element of `M` such that their result under `B` is non-zero.
More concisely: If `R` is a commutative ring, `M` and `M1` are `R`-modules with basis `v` such that every element in `v` is not self-orthogonal with respect to a bilinear map `B` from `M` to `M1`, then `B` is left-separating.
|
LinearMap.separatingRight_iff_flip_ker_eq_bot
theorem LinearMap.separatingRight_iff_flip_ker_eq_bot :
∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7}
[inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : CommSemiring R₁]
[inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁] [inst_6 : CommSemiring R₂] [inst_7 : AddCommMonoid M₂]
[inst_8 : Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M},
B.SeparatingRight ↔ LinearMap.ker B.flip = ⊥
The theorem `LinearMap.separatingRight_iff_flip_ker_eq_bot` states that for all types `R`, `R₁`, `R₂`, `M`, `M₁`, `M₂`, given that `R` is a commutative semiring, `M` is an additive commutative monoid over `R`, `R₁` is a commutative semiring, `M₁` is an additive commutative monoid over `R₁`, `R₂` is a commutative semiring, `M₂` is an additive commutative monoid over `R₂`, and if `I₁` and `I₂` are ring homomorphisms from `R₁` and `R₂` to `R` respectively, and `B` is a bilinear map from `M₁` to `M₂`, then `B` is right-separating if and only if the kernel of the flip of `B` is trivial (i.e., contains only the zero element). The flip of a map in this context refers to a new map that swaps the order of the arguments.
More concisely: Given commutative semirings R, R₁, R₂, additive commutative monoids M, M₁, M₂, ring homomorphisms I₁ from R₁ to R, I₂ from R₂ to R, and a bilinear map B from M₁ to M₂ over R, B is right-separating if and only if the kernel of the flip of B is the zero map.
|
LinearMap.IsOrthoᵢ.nondegenerate_of_not_isOrtho_basis_self
theorem LinearMap.IsOrthoᵢ.nondegenerate_of_not_isOrtho_basis_self :
∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {n : Type u_19} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] [inst_3 : AddCommGroup M₁] [inst_4 : Module R M₁] [inst_5 : NoZeroSMulDivisors R M₁]
{B : M →ₗ[R] M →ₗ[R] M₁} (v : Basis n R M),
B.IsOrthoᵢ ⇑v → (∀ (i : n), ¬B.IsOrtho (v i) (v i)) → B.Nondegenerate
This theorem states that given an orthogonal basis with respect to a bilinear map in a module over a commutative ring, the bilinear map is nondegenerate if no elements of the basis are self-orthogonal. In other words, for a basis that consists of orthogonal vectors with respect to a bilinear map, if none of these basis vectors are self-orthogonal, then the bilinear map does not map any non-zero vector to zero.
More concisely: Given an orthogonal basis for a bilinear form on a module over a commutative ring with no self-orthogonal vectors, the bilinear form is nondegenerate.
|
LinearMap.IsOrthoᵢ.separatingRight_iff_not_isOrtho_basis_self
theorem LinearMap.IsOrthoᵢ.separatingRight_iff_not_isOrtho_basis_self :
∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {n : Type u_19} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] [inst_3 : AddCommGroup M₁] [inst_4 : Module R M₁] [inst_5 : NoZeroSMulDivisors R M₁]
{B : M →ₗ[R] M →ₗ[R] M₁} (v : Basis n R M),
B.IsOrthoᵢ ⇑v → (∀ (i : n), ¬B.IsOrtho (v i) (v i)) → B.SeparatingRight
This theorem states that for an orthogonal basis with respect to a bilinear map, if none of the elements in the basis are self-orthogonal, then the bilinear map is right-separating. It is defined over a commutative ring `R`, modules `M` and `M₁` over `R`, and a basis `v` of `M`. The bilinear map is represented by `B`, which maps from `M` to the linear map from `M` to `M₁`. The orthogonality of the basis with respect to `B` is denoted by `B.IsOrthoᵢ ⇑v`, and the lack of self-orthogonality in the basis is represented by `∀ (i : n), ¬B.IsOrtho (v i) (v i)`. The theorem guarantees that under these conditions, the bilinear map `B` is right-separating, denoted by `B.SeparatingRight`.
More concisely: If `B` is a bilinear map over a commutative ring `R` on modules `M` and `M₁`, and `v` is a basis of `M` such that `B.IsOrthoᵢ ⇑v` holds for all pairs of distinct indices `i`, `j`, and `∀ (i : ℕ), ¬B.IsOrtho (v i) (v i)`, then `B` is right-separating.
|
LinearMap.not_separatingLeft_zero
theorem LinearMap.not_separatingLeft_zero :
∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} (M₁ : Type u_6) (M₂ : Type u_7)
[inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : CommSemiring R₁]
[inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁] [inst_6 : CommSemiring R₂] [inst_7 : AddCommMonoid M₂]
[inst_8 : Module R₂ M₂] (I₁ : R₁ →+* R) (I₂ : R₂ →+* R) [inst_9 : Nontrivial M₁], ¬LinearMap.SeparatingLeft 0
This theorem states that in a non-trivial module (a structure that generalizes vector spaces), the zero linear map cannot be separating from the left. In other words, there is no meaningful way to distinguish elements of the module solely based on their images under the zero map. This is because the zero map sends all elements of the module to the zero element, losing all information about the original element.
More concisely: In a non-trivial module, the zero linear map cannot separate elements.
|
LinearMap.nondegenerateRestrictOfDisjointOrthogonal
theorem LinearMap.nondegenerateRestrictOfDisjointOrthogonal :
∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : AddCommGroup M₁] [inst_4 : Module R M₁] {B : M →ₗ[R] M →ₗ[R] M₁},
B.IsRefl → ∀ {W : Submodule R M}, Disjoint W (W.orthogonalBilin B) → (B.domRestrict₁₂ W W).Nondegenerate
This theorem states that for a given commutative ring `R` and its two modules `M` and `M₁`, if `B` is a reflexive bilinear map from `M` to `M₁`, and `W` is a submodule of `M` such that `W` is disjoint from its orthogonal complement with respect to `B` (i.e., there is no element in `W` that is also in the orthogonal complement of `W`), then the restriction of `B` onto `W` is nondegenerate. In other words, there are no zero divisors in the restriction of `B` to `W`.
More concisely: If `B` is a reflexive bilinear map on commutative ring `R`'s modules `M` and `M₁`, and `W` is a submodule of `M` disjoint from `B`'s orthogonal complement, then the restriction of `B` to `W` is nondegenerate.
|
LinearMap.separatingLeft_iff_ker_eq_bot
theorem LinearMap.separatingLeft_iff_ker_eq_bot :
∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7}
[inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : CommSemiring R₁]
[inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁] [inst_6 : CommSemiring R₂] [inst_7 : AddCommMonoid M₂]
[inst_8 : Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M},
B.SeparatingLeft ↔ LinearMap.ker B = ⊥
This theorem states that for any commutative semiring `R`, additive commutative monoid `M`, module `R M`, commutative semiring `R₁`, additive commutative monoid `M₁`, module `R₁ M₁`, commutative semiring `R₂`, additive commutative monoid `M₂`, module `R₂ M₂`, and any bilinear map `B` from `M₁` to `M₂` to `M`, the map `B` is left-separating if and only if the kernel of `B` is trivial, i.e., it only contains the zero element. A left-separating map is one where if the map applied to any two different elements gives the same result, then the two original elements were identical. So, the theorem essentially tells us that a bilinear map separates distinct elements in its domain if and only if it doesn't map any non-zero elements to zero.
More concisely: A bilinear map between two commutative semimodules is left-separating if and only if its kernel is the trivial submonoid.
|
LinearMap.isCompl_span_singleton_orthogonal
theorem LinearMap.isCompl_span_singleton_orthogonal :
∀ {K : Type u_13} {V : Type u_16} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
{B : V →ₗ[K] V →ₗ[K] K} {x : V},
¬B.IsOrtho x x → IsCompl (Submodule.span K {x}) ((Submodule.span K {x}).orthogonalBilin B)
The theorem `LinearMap.isCompl_span_singleton_orthogonal` states that for any field `K` and additive commutative group `V` with `V` as a module over `K`, given a bilinear form `B` and an element `x` in `V` such that `B x x` is not zero, the span of the singleton set `{x}` is complement to its orthogonal complement with respect to the bilinear form `B`.
In other words, if `x` is a vector in a vector space `V` over a field `K`, and `B` is a bilinear form on `V` for which `B x x` is not zero, then the smallest subspace of `V` containing `x` is complementary to the subspace of all vectors orthogonal to `x` under `B`. This means that any vector in `V` can be uniquely written as a sum of a vector from the subspace spanned by `x` and a vector from the orthogonal complement.
More concisely: For any field `K`, additive commutative group `V` as a `K`-module, bilinear form `B` on `V`, and non-zero vector `x` in `V`, the subspace spanned by `{x}` is the orthogonal complement's complement with respect to `B`.
|
LinearMap.linearIndependent_of_isOrthoᵢ
theorem LinearMap.linearIndependent_of_isOrthoᵢ :
∀ {K : Type u_13} {K₁ : Type u_14} {V : Type u_16} {V₁ : Type u_17} {n : Type u_19} [inst : Field K]
[inst_1 : AddCommGroup V] [inst_2 : Module K V] [inst_3 : Field K₁] [inst_4 : AddCommGroup V₁]
[inst_5 : Module K₁ V₁] {I₁ I₁' : K₁ →+* K} {B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V} {v : n → V₁},
B.IsOrthoᵢ v → (∀ (i : n), ¬B.IsOrtho (v i) (v i)) → LinearIndependent K₁ v
This theorem states that a set of vectors `v`, which are orthogonal with respect to some sesquilinear map `B`, is linearly independent over a field `K₁` if for all indices `i`, the sesquilinear map `B` applied to `v i` and `v i` is non-zero. In other words, none of the vectors in the set `v` is orthogonal to itself under the map `B`. This is stated within the context of a field `K`, vector spaces `V` and `V₁` over `K` and `K₁` respectively, and two ring homomorphisms `I₁` and `I₁'` from `K₁` to `K`.
More concisely: A set of vectors `v` in a vector space over a field `K₁`, orthogonal with respect to a sesquilinear map `B` over a field `K`, is linearly independent if `B(vi, vi) ≠ 0` for all indices `i`.
|