comp — Mathlib

English

If σ12: R1 → R2 and σ23: R2 → R3 are surjective and satisfy RingHomCompTriple, then σ13: R1 → R3 is surjective.

Русский

Если σ12: R1 → R2 и σ23: R2 → R3 сюръективны и удовлетворяют RingHomCompTriple, то σ13: R1 → R3 сюръективен.

LaTeX

$$$\forall z \in R_3, \exists x \in R_1: \ σ_{13}(x) = z$$$

Lean4

/-- This cannot be an instance as there is no way to infer `σ₁₂` and `σ₂₃`. -/
theorem comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomSurjective σ₁₂] [RingHomSurjective σ₂₃] : RingHomSurjective σ₁₃ :=
  {
    is_surjective := by
      have := σ₂₃.surjective.comp σ₁₂.surjective
      rwa [← RingHom.coe_comp, RingHomCompTriple.comp_eq] at this }

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