English
A ker-tensor product equality expresses the compatibility between the kernel of a tensor product map and the range of the left-tensor map, consistent with right-exactness results.
Русский
Совместимость ядра тензорного отображения и образа левого тензорного отображения.
LaTeX
$$ker(TensorProduct.mk R (R ⧸ I) Q 1) = I • ⊤$$
Lean4
/-- The inverse map in `rTensor.equiv_of_rightInverse` (computably, given a right inverse) -/
noncomputable def inverse_of_rightInverse {h : P → N} (hfg : Exact f g) (hgh : Function.RightInverse h g) :
P ⊗[R] Q →ₗ[R] N ⊗[R] Q ⧸ LinearMap.range (rTensor Q f) :=
TensorProduct.lift
{ toFun := fun p ↦ Submodule.mkQ _ ∘ₗ TensorProduct.mk R _ _ (h p)
map_add' := fun p p' =>
LinearMap.ext fun q =>
(Submodule.Quotient.eq _).mpr <|
by
change h (p + p') ⊗ₜ[R] q - (h p ⊗ₜ[R] q + h p' ⊗ₜ[R] q) ∈ range (rTensor Q f)
rw [← TensorProduct.add_tmul, ← TensorProduct.sub_tmul]
apply le_comap_range_rTensor f
rw [exact_iff] at hfg
simp only [← hfg, mem_ker, map_sub, map_add, hgh _, sub_self]
map_smul' := fun r p =>
LinearMap.ext fun q =>
(Submodule.Quotient.eq _).mpr <|
by
change h (r • p) ⊗ₜ[R] q - r • h p ⊗ₜ[R] q ∈ range (rTensor Q f)
rw [TensorProduct.smul_tmul', ← TensorProduct.sub_tmul]
apply le_comap_range_rTensor f
rw [exact_iff] at hfg
simp only [← hfg, mem_ker, map_sub, map_smul, hgh _, sub_self] }
