multiple_mem_adjoin_of_mem_localization_adjoin

English

There is a finite instance ensuring that a Span over R' is controlled by Span over R.

Русский

Существует конечный пример, обеспечивающий контроль над span над R' знаменем над R.

LaTeX

$$$\\operatorname{Finite}\\;\\operatorname{Localization}\\;\\operatorname{Span}$$$

Lean4

/-- If `S` is an `R' = M⁻¹R` algebra, and `x ∈ adjoin R' s`,
then `t • x ∈ adjoin R s` for some `t : M`. -/
theorem multiple_mem_adjoin_of_mem_localization_adjoin [Algebra R' S] [Algebra R S] [IsScalarTower R R' S]
    [IsLocalization M R'] (s : Set S) (x : S) (hx : x ∈ Algebra.adjoin R' s) : ∃ t : M, t • x ∈ Algebra.adjoin R s :=
  by
  change ∃ t : M, t • x ∈ Subalgebra.toSubmodule (Algebra.adjoin R s)
  change x ∈ Subalgebra.toSubmodule (Algebra.adjoin R' s) at hx
  simp_rw [Algebra.adjoin_eq_span] at hx ⊢
  exact multiple_mem_span_of_mem_localization_span M R' _ _ hx

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