IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt
theorem IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt :
∀ {R K : Type u} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K] [inst_3 : IsAlgClosed K] {ι : Type u}
(v : ι → K) [inst_4 : Nontrivial R],
IsTranscendenceBasis R v →
Cardinal.mk R ≤ Cardinal.aleph0 → Cardinal.aleph0 < Cardinal.mk K → Cardinal.mk K = Cardinal.mk ι
The theorem states that if `K` is an uncountable algebraically closed field, with a given transcendence basis `v`, and `R` is a commutative ring whose cardinality is less than or equal to `ℵ₀` (the smallest infinite cardinal number), then the cardinality of `K` is equal to the cardinality of the index set of the transcendence basis. In other words, for such a field `K`, the size of any maximal algebraically independent subset (the transcendence basis) is equal to the size of the field itself, provided that the cardinality of the base ring `R` is at most countably infinite.
More concisely: If `K` is an uncountable algebraically closed field with transcendence basis `v` over a commutative ring `R` of cardinality less than or equal to `ℵ₀`, then the cardinality of `K` equals that of `v`.
|
IsAlgClosed.ringEquivOfCardinalEqOfCharZero
theorem IsAlgClosed.ringEquivOfCardinalEqOfCharZero :
∀ {K L : Type} [inst : Field K] [inst_1 : Field L] [inst_2 : IsAlgClosed K] [inst_3 : IsAlgClosed L]
[inst_4 : CharZero K] [inst_5 : CharZero L],
Cardinal.aleph0 < Cardinal.mk K → Cardinal.mk K = Cardinal.mk L → Nonempty (K ≃+* L)
The theorem states that if we have two uncountable algebraically closed fields, K and L, both of characteristic zero, and they have the same cardinality (that is, the same number of elements), then there exists a ring isomorphism between them. In other words, we can set up a one-to-one correspondence between the elements of K and L that preserves addition, multiplication, and the multiplicative identity. The term "uncountable" here means that the cardinality of the fields are strictly greater than the cardinality of the set of natural numbers, denoted by `ℵ₀` in the theorem.
More concisely: If two uncountable, algebraically closed fields of characteristic zero with the same uncountable cardinality are given, there exists a ring isomorphism between them.
|
Algebra.IsAlgebraic.cardinal_mk_le_max
theorem Algebra.IsAlgebraic.cardinal_mk_le_max :
∀ (R L : Type u) [inst : CommRing R] [inst_1 : CommRing L] [inst_2 : IsDomain L] [inst_3 : Algebra R L]
[inst_4 : NoZeroSMulDivisors R L],
Algebra.IsAlgebraic R L → Cardinal.mk L ≤ max (Cardinal.mk R) Cardinal.aleph0
The theorem `Algebra.IsAlgebraic.cardinal_mk_le_max` states that for any Commutative Ring `R` and any Commutative Ring `L` that also forms a domain and does not contain zero divisors under scalar multiplication, if `L` is an algebraic extension of `R`, then the cardinality of `L` is less than or equal to the maximum of the cardinality of `R` and `ℵ₀` (the smallest infinite cardinal number). In simpler terms, the size of an algebraic extension of a ring is no larger than the larger of the size of the base ring or the size of the set of natural numbers.
More concisely: If `R` is a commutative ring, `L` is a commutative domain and algebraic extension of `R` without zero divisors under scalar multiplication, then `|L| ≤ max(|R|, ℵ₀)`.
|
IsAlgClosed.ringEquivOfCardinalEqOfCharEq
theorem IsAlgClosed.ringEquivOfCardinalEqOfCharEq :
∀ {K L : Type} [inst : Field K] [inst_1 : Field L] [inst_2 : IsAlgClosed K] [inst_3 : IsAlgClosed L] (p : ℕ)
[inst_4 : CharP K p] [inst_5 : CharP L p],
Cardinal.aleph0 < Cardinal.mk K → Cardinal.mk K = Cardinal.mk L → Nonempty (K ≃+* L)
The theorem `IsAlgClosed.ringEquivOfCardinalEqOfCharEq` states that, for any two uncountable algebraically closed fields `K` and `L` which have the same characteristic `p` and the same cardinality, there exists a ring isomorphism between them. Here, uncountable is defined in terms of the cardinality of the fields being greater than the cardinality of the set of natural numbers `ℵ₀`.
More concisely: For uncountable algebraically closed fields K and L of equal characteristic and cardinality greater than that of the set of natural numbers, there exists a ring isomorphism between them.
|