lTensor_surjective — Mathlib

English

The map lTensor(Q,g) is surjective whenever g is surjective; the corresponding exactness result yields left-exactness for the tensor product functor.

Русский

Отображение lTensor(Q,g) сюръективно, если g сюръективно; соответствующий результат точности дает левую точность тензорного функторa.

LaTeX

$$$$ \text{If } g ext{ is surjective, then } l_{Q} g ext{ is surjective.} $$$$

Lean4

/-- If `g` is surjective, then `lTensor Q g` is surjective -/
theorem lTensor_surjective (hg : Function.Surjective g) : Function.Surjective (lTensor Q g) :=
  by
  intro z
  induction z with
  | zero => exact ⟨0, map_zero _⟩
  | tmul q p =>
    obtain ⟨n, rfl⟩ := hg p
    exact ⟨q ⊗ₜ[R] n, rfl⟩
  | add x y hx hy =>
    obtain ⟨x, rfl⟩ := hx
    obtain ⟨y, rfl⟩ := hy
    exact ⟨x + y, map_add _ _ _⟩

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