strongRankCondition_iff_succ
theorem strongRankCondition_iff_succ :
∀ (R : Type u) [inst : Semiring R],
StrongRankCondition R ↔ ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Function.Injective ⇑f
A ring `R` satisfies the strong rank condition if and only if, for every natural number `n`, any linear map from `(Fin (n + 1) → R)` to `(Fin n → R)` is not injective. That is, there does not exist a linear map that preserves distinctness when mapping from a finite set of size `n+1` to a finite set of size `n` under semiring `R`. Here, a function is considered injective if whenever it maps two different inputs to the same output, then those inputs must have been the same to begin with.
More concisely: A ring satisfies the strong rank condition if and only if no linear map exists from `(Fin n + 1)` to `(Fin n)` over the semiring `R` that preserves distinct inputs.
|
RankCondition.le_of_fin_surjective
theorem RankCondition.le_of_fin_surjective :
∀ {R : Type u} [inst : Semiring R] [self : RankCondition R] {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R),
Function.Surjective ⇑f → m ≤ n
This theorem states that for any surjective linear map `f` from `Rⁿ` to `Rᵐ` over a semiring `R`, the dimension `m` of the codomain is less than or equal to the dimension `n` of the domain. In other words, if every element of `Rᵐ` can be mapped to from `Rⁿ` using `f`, then the number of dimensions in `Rᵐ` (`m`) must be less than or equal to the number of dimensions in `Rⁿ` (`n`). This is known as the rank condition.
More concisely: If `f` is a surjective linear map from `Rⁿ` to `Rᵐ` over a semiring `R`, then `n` ≥ `m`. (The rank condition states that the dimension of the codomain is less than or equal to the dimension of the domain in the more common setting where `R` is a field.)
|
InvariantBasisNumber.eq_of_fin_equiv
theorem InvariantBasisNumber.eq_of_fin_equiv :
∀ {R : Type u} [inst : Semiring R] [self : InvariantBasisNumber R] {n m : ℕ},
((Fin n → R) ≃ₗ[R] Fin m → R) → n = m
The theorem `InvariantBasisNumber.eq_of_fin_equiv` states that given any semiring `R`, and any two natural numbers `n` and `m`, if there exists a linear equivalence between the function spaces `Fin n → R` and `Fin m → R` (essentially representing `Rⁿ` and `Rᵐ` respectively), then `n` must be equal to `m`. This theorem is a formal statement of the Invariant Basis Number property in Mathematics, which asserts that the dimension of a vector space is unique.
More concisely: Given any semiring R and two natural numbers n and m, if there exists a linear equivalence between the function spaces Fin n -> R and Fin m -> R, then n = m. (This theorem asserts the uniqueness of the dimension of a vector space over a semiring.)
|
StrongRankCondition.le_of_fin_injective
theorem StrongRankCondition.le_of_fin_injective :
∀ {R : Type u} [inst : Semiring R] [self : StrongRankCondition R] {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R),
Function.Injective ⇑f → n ≤ m
The theorem `StrongRankCondition.le_of_fin_injective` states that for any injective linear map `f` from `Rⁿ` to `Rᵐ` over a semiring `R` satisfying the strong rank condition, the dimension of the domain `n` is less than or equal to the dimension of the codomain `m`. In simpler terms, if you have a function that maps points from an `n`-dimensional space to an `m`-dimensional space without merging any points (i.e., the function is injective), then `n` must be less than or equal to `m`. This is a statement about the dimensionality restrictions for such injective linear transformations.
More concisely: If `f` is an injective linear map from `Rⁿ` to `Rᵐ` over a semiring `R` satisfying the strong rank condition, then `n ≤ m`.
|
le_of_fin_injective
theorem le_of_fin_injective :
∀ (R : Type u) [inst : Semiring R] [inst_1 : StrongRankCondition R] {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R),
Function.Injective ⇑f → n ≤ m
This theorem, named `le_of_fin_injective`, states that for any semiring `R` with a strong rank condition, if we have a linear map `f` from functions from `Fin n` to `R` to functions from `Fin m` to `R`, and this map `f` is injective, then `n` is less than or equal to `m`. In other words, the dimension of the domain of an injective linear map cannot exceed the dimension of the codomain, when the coefficient ring has a strong rank condition.
More concisely: For any semiring with a strong rank condition, an injective linear map from functions on a finite set of size n to the semiring to functions on a finite set of size m implies n <= m.
|
le_of_fin_surjective
theorem le_of_fin_surjective :
∀ (R : Type u) [inst : Semiring R] [inst_1 : RankCondition R] {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R),
Function.Surjective ⇑f → m ≤ n
The theorem `le_of_fin_surjective` states that for any semiring `R` that satisfies the rank condition and for any natural numbers `n` and `m`, if there exists a linear map `f` from the set of functions `Fin n → R` to the set of functions `Fin m → R` that is surjective (i.e., for each function from `Fin m` to `R`, there is a function from `Fin n` to `R` that maps to it under `f`), then `m` is less than or equal to `n`. In essence, this theorem says that the dimension of the target space cannot exceed the dimension of the source space if the linear map is surjective.
More concisely: If there exists a surjective linear map from functions `Fin n -> R` to functions `Fin m -> R` in a semiring `R` satisfying the rank condition, then `n` greater than or equal to `m`.
|
eq_of_fin_equiv
theorem eq_of_fin_equiv :
∀ (R : Type u) [inst : Semiring R] [inst_1 : InvariantBasisNumber R] {n m : ℕ},
((Fin n → R) ≃ₗ[R] Fin m → R) → n = m
This theorem, `eq_of_fin_equiv`, states that for any type `R` equipped with a semiring structure and an invariant basis number property, if there is a linear equivalence between the functions from `Fin n` to `R` and `Fin m` to `R`, then `n` must be equal to `m`. Here, `Fin n` is the type of finite ordinals less than `n`, so this theorem essentially relates to the linear structure of finite-dimensional vector spaces over the ring `R`.
More concisely: If there exists a linear equivalence between `Fin n` and `Fin m` as `R`-modules, then `n = m`.
|