ModuleConnectedSource.lean
Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.ConnectedSource
2 declarations indexed from sourceView source ↗ Module documentation
A connected generic fibre of an open morphism
The generic fibre of an open morphism to an irreducible scheme is dense in the source. If that fibre is geometrically connected, its image is connected and dense, so the source is connected as well.
For Remark 2.3 this supplies the connectedness of the smooth arithmetic scheme E from the geometric connectedness of E_ℚ. Smoothness gives universal openness through flatness and local finite presentation. Neither properness nor connectedness of every special fibre is assumed here.
Imports6
- Mathlib.AlgebraicGeometry.Fiber
- Mathlib.AlgebraicGeometry.Geometrically.Connected
- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
- Mathlib.Topology.Connected.Basic
- Mathlib.Topology.Maps.Basic
- Mathlib.Topology.Sober
Imported by2
Declarations
AlgebraicGeometry.Scheme.Hom.denseRange_genericFiberι_of_isOpenMap
DocumentationThe inclusion of the generic fibre of an open morphism to an irreducible scheme has dense range.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AlgebraicGeometry.Scheme.Hom
open CategoryTheory TopologicalSpace
universe u
AlgebraicGeometry.Scheme.Hom.connectedSpace_of_geometricallyConnected_genericFiber
DocumentationFor a universally open morphism to an irreducible base, a geometrically connected generic fibre forces the source itself to be connected.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AlgebraicGeometry.Scheme.Hom
open CategoryTheory TopologicalSpace
universe u