English
Fix f: M → N, g: N → P with Exact f g and a surjective right inverse h of g. Then there is a linear map lTensor.inverse_of_rightInverse: (Q ⊗_R P) →_R (N ⊗_R Q) / range (lTensor Q f) serving as the inverse to the forward map lTensor Q g in the quotient construction, making the pair a linear equivalence.
Русский
Пусть f: M → N, g: N → P образуют точную последовательность и есть правый обратный h к g. Тогда существует линейное отображение lTensor.inverse_of_rightInverse: (Q ⊗ P) → (N ⊗ Q) / range(lTensor Q f), являющееся обратным к прямому отображению lTensor Q g в конструкцию квантизирования, образуя линейное эквивалентное отображение.
LaTeX
$${ h : P → N } → (f,g,h) дают существование линейного отображения\nlTensor.inverse_of_rightInverse Q hfg hgh : Q ⊗ P → (Q ⊗ N)/range(lTensor Q f)$$
Lean4
/-- The inverse map in `lTensor.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) :
Q ⊗[R] P →ₗ[R] Q ⊗[R] N ⧸ LinearMap.range (lTensor Q f) :=
TensorProduct.lift <|
LinearMap.flip <|
{ toFun := fun p ↦ Submodule.mkQ _ ∘ₗ ((TensorProduct.mk R _ _).flip (h p))
map_add' := fun p p' =>
LinearMap.ext fun q =>
(Submodule.Quotient.eq _).mpr <|
by
change q ⊗ₜ[R] (h (p + p')) - (q ⊗ₜ[R] (h p) + q ⊗ₜ[R] (h p')) ∈ range (lTensor Q f)
rw [← TensorProduct.tmul_add, ← TensorProduct.tmul_sub]
apply le_comap_range_lTensor 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 q ⊗ₜ[R] (h (r • p)) - r • q ⊗ₜ[R] (h p) ∈ range (lTensor Q f)
rw [← TensorProduct.tmul_smul, ← TensorProduct.tmul_sub]
apply le_comap_range_lTensor f
rw [exact_iff] at hfg
simp only [← hfg, mem_ker, map_sub, map_smul, hgh _, sub_self] }
