of_retract — Mathlib

English

A retract of a flat module is flat (simplified statement).

Русский

Обрезанный модуль плоский.

LaTeX

$$$\text{of_retract }(i,r,h): Flat R N$$$

Lean4

/-- A retract of a flat `R`-module is flat. -/
theorem of_retract [f : Flat R M] (i : N →ₗ[R] M) (r : M →ₗ[R] N) (h : r.comp i = LinearMap.id) : Flat R N :=
  by
  rw [iff_rTensor_injectiveₛ] at *
  refine fun P _ _ Q ↦ .of_comp (f := lTensor P i) ?_
  rw [← coe_comp, lTensor_comp_rTensor, ← rTensor_comp_lTensor, coe_comp]
  refine (f Q).comp (Function.RightInverse.injective (g := lTensor Q r) fun x ↦ ?_)
  simp [← comp_apply, ← lTensor_comp, h]

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