starMap_surjective — Mathlib

English

If φ is surjective, then starMap φ is surjective as a map between unitizations.

Русский

Если φ сюръективен, то starMap φ сюръективен как отображение между единичизациями.

LaTeX

$$$\text{Surj}(φ) \Rightarrow \text{Surj}(\text{starMap}(φ)).$$$

Lean4

/-- If `φ : A →⋆ₙₐ[R] B` is surjective, the lift
`starMap φ : Unitization R A →⋆ₐ[R] Unitization R B` is also surjective. -/
theorem starMap_surjective {φ : A →⋆ₙₐ[R] B} (hφ : Function.Surjective φ) : Function.Surjective (starMap φ) :=
  by
  intro x
  induction x using Unitization.ind with
  | inl_add_inr r b =>
    obtain ⟨a, rfl⟩ := hφ b
    exact ⟨(r, a), by rfl⟩

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