surjective_comp_left_of_exists_rightInverse

English

If there exists a right-inverse f' to f, then composing with f on the left yields a surjective map on the domain of linear maps, i.e., the map g ↦ f ∘ g is surjective given f' with f ∘ f' = id.

Русский

Если существует правый обратный к f, то отображение g ↦ f ∘ g по левому слою является сюръективным, то есть существует g' such что f ∘ g' = заданная функция.

LaTeX

$$Exists f' with f ∘ f' = id → Surjective (λ g, f ∘ g)$$

Lean4

theorem surjective_comp_left_of_exists_rightInverse {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₂₃ σ₃₂]
    [RingHomCompTriple σ₁₃ σ₃₂ σ₁₂] (hf : ∃ f' : M₃ →ₛₗ[σ₃₂] M₂, f.comp f' = .id) :
    Surjective fun g : M₁ →ₛₗ[σ₁₂] M₂ ↦ f.comp g := by
  intro h
  obtain ⟨f', hf'⟩ := hf
  refine ⟨f'.comp h, ?_⟩
  simp_rw [← comp_assoc, hf', id_comp]

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