exists_basis_of_span_of_flat — Mathlib

English

If M is finitely presented and flat, then there exists a basis corresponding to a given generating set under a base-change.

Русский

Если M — конечная презентация и плоский, существует база, соответствующая заданному порождающему множеству при базовом изменении.

LaTeX

$$$ \exists \kappa (a: \kappa \to M) (b: Basis \kappa R M), \; \forall i, b i = a i. $$$

Lean4

theorem exists_basis_of_span_of_flat [Module.FinitePresentation R M] [Module.Flat R M] {ι : Type u} (v : ι → M)
    (hv : Submodule.span R (Set.range v) = ⊤) : ∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ i, b i = v (a i) :=
  exists_basis_of_span_of_maximalIdeal_rTensor_injective
    (Module.Flat.rTensor_preserves_injective_linearMap (𝔪).subtype Subtype.val_injective) v hv

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