ofIsLocalizedModule — Mathlib

English

If M has a basis over R and we localize at S, there is a localized basis for Mₛ over Rₛ, obtained by transporting the original basis via the localized map f.

Русский

Если в модуле M есть базис над R и локализация существует, то существует локализованный базис Mₛ над Rₛ, получаемый переносом базиса через локализационное отображение f.

LaTeX

$$Module.Basis.ofIsLocalizedModule$$

Lean4

/-- If `M` has an `R`-basis, then localizing `M` at `S` has a basis over `R` localized at `S`. -/
noncomputable def ofIsLocalizedModule : Basis ι Rₛ Mₛ :=
  .mk (b.linearIndependent.of_isLocalizedModule Rₛ S f) <| by
    rw [Set.range_comp, span_eq_top_of_isLocalizedModule Rₛ S _ b.span_eq]

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