equivTensorQuot_naturality — Mathlib

English

If f is surjective, then map r f is surjective as well.

Русский

Если отображение f сюръектно, то и отображение map r f сюръективно.

LaTeX

$$$$ (\forall x', \exists x, map\_r f(x) = x') \Rightarrow (\forall y', \exists y, map\_r f(y)=y') $$$$

Lean4

theorem equivTensorQuot_naturality (f : M →ₗ[R] M') :
    equivTensorQuot r M' ∘ₗ map r f = f.rTensor (R ⧸ Ideal.span { r }) ∘ₗ equivTensorQuot r M :=
  quot_hom_ext _ _ _ (equivTensorQuot_naturality_mk r f)

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