Module

GeometricallyIrreducibleConnected.lean

Nyll.SchemeTheory.Morphisms.GeometricallyIrreducibleConnected

1 declaration indexed from sourceView source ↗

Module documentation

Geometric irreducibility implies geometric connectedness

A geometrically irreducible morphism has connected fibres after every field base change.

Imports2

Mathlib.AlgebraicGeometry.Geometrically.Connected
Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Imported by3

theorem

geometricallyConnected

L30 ↗

AlgebraicGeometry.GeometricallyIrreducible.geometricallyConnected

Source context 4 commands

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

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

Lean source · statement

theorem _root_.AlgebraicGeometry.GeometricallyIrreducible.geometricallyConnected {X Y :
    Scheme.{u}} (f : X ⟶ Y)
    [GeometricallyIrreducible f] : GeometricallyConnected f

Module documentation

Geometric irreducibility implies geometric connectedness

Declarations

geometricallyConnected