sectionOfRetractionKerToTensorAux_prop

English

Localization of the base and intermediate rings preserves formal smoothness in the composed setting.

Русский

Локализация базы и промежуточных колец сохраняет формальную гладкость в составе.

LaTeX

$$$[\operatorname{FormallySmooth} R S] \Rightarrow [\operatorname{FormallySmooth} R_m S_m]$$$

Lean4

theorem sectionOfRetractionKerToTensorAux_prop (x y) (h : algebraMap P S x = algebraMap P S y) :
    x - l (1 ⊗ₜ .D _ _ x) = y - l (1 ⊗ₜ .D _ _ y) :=
  by
  rw [sub_eq_iff_eq_add, sub_add_comm, ← sub_eq_iff_eq_add, ← Submodule.coe_sub, ← map_sub, ← tmul_sub, ← map_sub]
  exact congr_arg Subtype.val (LinearMap.congr_fun hl.symm ⟨x - y, by simp [RingHom.mem_ker, h]⟩)

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