English
The inverse (symmetry) of the kernel–tensor correspondence respects subtype structure, giving equality on the subtype side.
Русский
Обратная сторона соответствия ядро-тензор сохраняет структуру подтипа, приводя к равенству на стороне подтипа.
LaTeX
$$$(lTensor M (ker f).subtype) ((tensorKerEquiv S M f).symm x) = x$ for x in ker(lTensor S M f)$$
Lean4
/-- If `M` is `R`-flat, the canonical map `M ⊗[R] ker f →ₗ[R] ker (𝟙 ⊗ f)` is an isomorphism. -/
def tensorKerEquiv [Module.Flat R M] : M ⊗[R] LinearMap.ker f ≃ₗ[S] LinearMap.ker (AlgebraTensorModule.lTensor S M f) :=
LinearEquiv.ofLinear (LinearMap.tensorKer S M f) (LinearMap.tensorKerInv S M f) (by ext x; simp)
(by
ext m x
apply (Module.Flat.lTensor_preserves_injective_linearMap (ker f).subtype (ker f).injective_subtype)
simp)
