ModuleConnectedOfGlobalSections.lean
Nyll.SchemeTheory.Affine.ConnectedOfGlobalSections
3 declarations indexed from sourceView source ↗ Module documentation
Connectedness from integral global sections
A disconnection of a scheme produces a nontrivial idempotent global section by gluing the constant sections zero and one. Consequently, a scheme whose ring of global sections is a domain is connected. In particular, a scheme over a field is connected when its actual global-sections map is an isomorphism. This is the section-to-connectedness step used for the fibres of the canonical relative normalization.
Imports7
- Mathlib.AlgebraicGeometry.Limits
- Mathlib.AlgebraicGeometry.Scheme
- Mathlib.Algebra.GroupWithZero.Idempotent
- Mathlib.Algebra.Ring.Equiv
- Mathlib.Topology.Connected.Clopen
- Mathlib.Topology.Sheaves.SheafCondition.Sites
- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Imported by3
Declarations
AlgebraicGeometry.Scheme.preconnectedSpace_of_globalSections_idempotents
DocumentationTriviality of actual global idempotent sections makes a scheme preconnected.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
AlgebraicGeometry.Scheme.connectedSpace_of_isDomain_globalSections
DocumentationA scheme with an integral domain of global sections is connected.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
AlgebraicGeometry.connectedSpace_of_isIso_appTop_to_field
DocumentationIf the actual global-sections map of a scheme over a field is an isomorphism, the scheme is connected.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u