Module

SurjectiveSectionPushout.lean

Nyll.SchemeTheory.Affine.SurjectiveSectionPushout

1 declaration indexed from sourceView source ↗

Module documentation

Surjectivity in an actual ring-section pushout

This applies native stability of surjective ring maps to the actual categorical pushout, retaining all four supplied maps.

Imports2

Mathlib.Algebra.Category.Ring.Constructions
Mathlib.RingTheory.RingHom.Surjective

Imported by1

Nyll.SchemeTheory.Affine.All

theorem

surjective_pushout_inr_of_surjective

L24 ↗

CommRingCat.surjective_pushout_inr_of_surjective

Documentation

In an actual ring pushout, the cobase change of a surjective map is surjective.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits
namespace CommRingCat
universe u

Lean source · statement

theorem surjective_pushout_inr_of_surjective
    {R S A B : CommRingCat.{u}} (f : R ⟶ S) (g : R ⟶ A)
    (i : S ⟶ B) (j : A ⟶ B) (h : IsPushout f g i j)
    (hf : Function.Surjective f) : Function.Surjective j

Module documentation

Surjectivity in an actual ring-section pushout

Declarations

surjective_pushout_inr_of_surjective