trdeg_le_cardinalMk — Mathlib

English

Under NoZeroDivisors and FaithfulSMul, for any s with adjoin algebraic over A, there exists t ⊆ s forming a transcendence basis.

Русский

При отсутствии нулей делимости и надёжном действии, для любого s с условием алгебраического над adjoin_R s, существует t ⊆ s образующий трансцендентный базис.

LaTeX

$$$ [NoZeroDivisors A] [FaithfulSMul R A] (s : Set A) [Algebra.IsAlgebraic (adjoin R s) A] : \\exists t, t \\subseteq s ∧ IsTranscendenceBasis R ((↑) : t \\to A) $$$

Lean4

theorem trdeg_le_cardinalMk [alg : Algebra.IsAlgebraic (adjoin R s) A] : trdeg R A ≤ #s :=
  by
  by_cases h : Injective (algebraMap R A)
  on_goal 2 => simp [trdeg_eq_zero_of_not_injective h]
  have := isDomain_of_adjoin_range R s
  have := (faithfulSMul_iff_algebraMap_injective R A).mpr h
  rw [← matroid_spanning_iff, ← matroid_cRank_eq] at *
  exact alg.cRank_le_cardinalMk

Похожие утверждения