Module

RadicialDescent.lean

Nyll.SchemeTheory.Morphisms.RadicialDescent

1 declaration indexed from sourceView source ↗

Module documentation

Descent of universal injectivity through a surjective morphism

The map between the two diagonal objects induced by a surjective morphism is surjective. Thus surjectivity of the diagonal of a composite implies surjectivity of the diagonal of its second factor.

Imports4

Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Imported by3

theorem

of_comp_surjective

L31 ↗

AlgebraicGeometry.UniversallyInjective.of_comp_surjective

Documentation

Universal injectivity descends through a surjective first factor.

Source context 4 commands

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

@[expose] public section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.UniversallyInjective

Lean source · statement

theorem of_comp_surjective {X Y Z : Scheme.{u}}
    (t : X ⟶ Y) (g : Y ⟶ Z) [Surjective t] [UniversallyInjective (t ≫ g)] :
    UniversallyInjective g

Module documentation

Descent of universal injectivity through a surjective morphism

Declarations

of_comp_surjective