Cardinality of a transcendence basis

This file concerns the cardinality of a transcendence basis.

References

• Stacks: Transcendence

TODO

Define the transcendence degree and show it is independent of the choice of a transcendence basis.

Tags

transcendence basis, transcendence degree, transcendence

theorem IsTranscendenceBasis.lift_cardinalMk_eq_max_lift {F : Type u} {E : Type v} [CommRing F] [Nontrivial F] [CommRing E] [IsDomain E] [Algebra F E] {ι : Type w} {x : ι → E} [Nonempty ι] (hx : IsTranscendenceBasis F x) : Cardinal.lift.{max u w, v} (Cardinal.mk E) = Cardinal.lift.{max v w, u} (Cardinal.mk F) ⊔ Cardinal.lift.{max u v, w} (Cardinal.mk ι) ⊔ Cardinal.aleph0

theorem IsTranscendenceBasis.lift_rank_eq_max_lift {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {ι : Type w} {x : ι → E} [Nonempty ι] (hx : IsTranscendenceBasis F x) : Cardinal.lift.{max u w, v} (Module.rank F E) = Cardinal.lift.{max v w, u} (Cardinal.mk F) ⊔ Cardinal.lift.{max u v, w} (Cardinal.mk ι) ⊔ Cardinal.aleph0

theorem Algebra.Transcendental.rank_eq_cardinalMk (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.Transcendental F E] : Module.rank F E = Cardinal.mk E

theorem IntermediateField.rank_sup_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) : Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B