Module

GeometricallyConnected_of_comp_of_surjective.lean

Nyll.AlgebraicCurves.Geometry.Curves.GeometricallyConnected_of_comp_of_surjective

1 declaration indexed from sourceView source ↗

Module documentation

Geometric connectedness descends through a surjective morphism

If a composite is geometrically connected and its first map is surjective, the second map is geometrically connected.

Imports1

Mathlib.AlgebraicGeometry.Geometrically.Connected

Imported by4

theorem

of_comp_of_surjective

L31 ↗

AlgebraicGeometry.GeometricallyConnected.of_comp_of_surjective

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.GeometricallyConnected_of_comp_of_surjective
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.GeometricallyConnected.of_comp_of_surjective {X Y Z : Scheme.{u}}
    (f : X ⟶ Y) (g : Y ⟶ Z) [GeometricallyConnected (f ≫ g)] [Surjective f] :
    GeometricallyConnected g

Module documentation

Geometric connectedness descends through a surjective morphism

Declarations

of_comp_of_surjective