surjective_isStableUnderBaseChange

English

Surjectivity is stable under base change: the base-changed map remains surjective.

Русский

Суръективность устойчива при базовой смене: полученная по основанию карта сохраняет суръективность.

LaTeX

$$$$ \operatorname{IsStableUnderBaseChange}( \text{surjective} ). $$$$

Lean4

theorem surjective_isStableUnderBaseChange : IsStableUnderBaseChange surjective :=
  by
  refine IsStableUnderBaseChange.mk surjective_respectsIso ?_
  classical
  introv h x
  induction x with
  | zero => exact ⟨0, map_zero _⟩
  | tmul x y =>
    obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
    rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
  | add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩

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