equivQuotTensor_naturality — Mathlib

English

Naturality of the tensor–quotient equivalence with respect to f.

Русский

Естественность тензорно-квотной эквивалентности по отношению к f.

LaTeX

$$$$ \text{equivQuotTensor}(r,M') \circ map_r f = f\otimes (R/(r)) \circ \text{equivQuotTensor}(r,M). $$$$

Lean4

theorem equivQuotTensor_naturality (f : M →ₗ[R] M') :
    equivQuotTensor r M' ∘ₗ map r f = f.lTensor (R ⧸ Ideal.span { r }) ∘ₗ equivQuotTensor r M :=
  quot_hom_ext _ _ _ (equivQuotTensor_naturality_mk r f)

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