Module

GeometricallyConnected_descendsAlong_surjective.lean

Nyll.AlgebraicCurves.Geometry.Curves.GeometricallyConnected_descendsAlong_surjective

2 declarations indexed from sourceView source ↗

Module documentation

Geometrically Connected descends Along surjective

Imports2

Mathlib.AlgebraicGeometry.Geometrically.Connected
Mathlib.CategoryTheory.MorphismProperty.Descent

Imported by3

theorem

geometricallyConnected_of_pullback_snd

L36 ↗

AlgebraicCurves.Geometry.Curves.Proofs.GeometricallyConnected_descendsAlong_surjective.AlgebraicGeometry.GeometricallyConnectedDescentAux.geometricallyConnected_of_pullback_snd

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.GeometricallyConnected_descendsAlong_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MorphismProperty
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace GeometricallyConnectedDescentAux
open _root_.AlgebraicGeometry

Lean source · statement

theorem geometricallyConnected_of_pullback_snd {X S S' : Scheme.{u}} (f : X ⟶ S) (σ : S' ⟶ S)
  [Surjective σ]
    [hgc : GeometricallyConnected (pullback.snd f σ)] : GeometricallyConnected f

theorem

descendsAlong_surjective

L63 ↗

AlgebraicGeometry.GeometricallyConnected.descendsAlong_surjective

Source context 7 commands