English
If f and g form an IsTensorProduct, then under flatness assumptions, the map hf.map hg LinearMap.id is injective when i is injective.
Русский
Если f и g образуют IsTensorProduct, то при плоскостях отображение hf.map hg LinearMap.id инъективно, когда i инъективно.
LaTeX
$$$\\text{Injective}(hf.map\\, hg\\, LinearMap.id)$ under hypotheses: IsTensorProduct f, IsTensorProduct g, i injective, [Module.Flat ...]$$
Lean4
theorem map_id_injective_of_flat_left {g : M₁ →ₗ[R] N₂ →ₗ[R] N} (hg : IsTensorProduct g) (i : M₂ →ₗ[R] N₂)
(hi : Function.Injective i) [Module.Flat R M₁] : Function.Injective (hf.map hg LinearMap.id i) :=
by
have h : hf.map hg LinearMap.id i = hg.equiv ∘ i.lTensor M₁ ∘ hf.equiv.symm :=
funext fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ hx hy ↦ by simp [hx, hy])
simpa [h] using Module.Flat.lTensor_preserves_injective_linearMap i hi
