instTensorProduct — Mathlib

English

Free modules over discrete types are flat (revisited).

Русский

Свободные модули над дискретными типами плоски (повтор).

LaTeX

$$$Flat\ R\ (\iota\to\_0 R)$$$

Lean4

instance {S} [CommSemiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] [Flat S M] [Flat R N] :
    Flat S (M ⊗[R] N) :=
  iff_rTensor_injectiveₛ.mpr fun P _ _ I ↦
    by
    letI := RestrictScalars.moduleOrig R S P
    change Submodule S (RestrictScalars R S P) at I
    change Function.Injective (rTensor _ I.subtype)
    simpa [AlgebraTensorModule.rTensor_tensor] using
      rTensor_preserves_injective_linearMap (.restrictScalars R <| I.subtype.rTensor M)
        (rTensor_preserves_injective_linearMap _ I.injective_subtype)

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