isAlgebraic_iff_exists_isTranscendenceBasis_subset

English

For an IsDomain A and FaithfulSMul over R, IsAlgebraic(adjoin_R s) A is equivalent to the existence of a subset t ⊆ s which forms a transcendence basis for A over R.

Русский

Для области A и отображения FaithfulSMul над R, IsAlgebraic(adjoin_R s) A эквивалентно существованию подмножества t ⊆ s, образующего трансцендентный базис A над R.

LaTeX

$$$ [IsDomain A] [FaithfulSMul R A] {s : Set A} : \\mathrm{Algebra.IsAlgebraic}(\\operatorname{adjoin}_R s) A \\iff \\exists t, t \\subseteq s \\land IsTranscendenceBasis R ((\\uparrow) : t \\to A) $$$

Lean4

theorem isAlgebraic_iff_exists_isTranscendenceBasis_subset [IsDomain A] [FaithfulSMul R A] {s : Set A} :
    Algebra.IsAlgebraic (adjoin R s) A ↔ ∃ t, t ⊆ s ∧ IsTranscendenceBasis R ((↑) : t → A) :=
  by
  simp_rw [← matroid_spanning_iff, ← matroid_isBase_iff, and_comm (a := _ ⊆ _)]
  exact Matroid.spanning_iff_exists_isBase_subset (subset_univ _)

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