free_of_flat_of_isLocalRing — Mathlib

English

If M and N are modules over a local ring with appropriate hypotheses, then a splitting injective map exists and leads to freeness of certain modules.

Русский

При подходящих гипотезах для модулей M и N над локальным кольцом существует разложимая инъекция, приводящая к свободности некоторых модулей.

LaTeX

$$$ \exists l', \; l' \circ l = id \Rightarrow Free_R(P). $$$

Lean4

@[stacks 00NZ]
theorem free_of_flat_of_isLocalRing [Module.Finite R P] [Flat R P] : Free R P :=
  let w := Free.chooseBasis k (k ⊗[R] P)
  have ⟨v, eq⟩ := (TensorProduct.mk_surjective R P k Quotient.mk_surjective).comp_left w
  .of_basis <|
    .mk (IsLocalRing.linearIndependent_of_flat _ (eq ▸ w.linearIndependent)) <| by
      exact (span_eq_top_of_tmul_eq_basis _ w <| congr_fun eq).ge

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