ModuleGenericFieldSource.lean
Nyll.EtaleFundamentalGroups.Normalization.GenericFieldSource
4 declarations indexed from sourceView source ↗ Module documentation
Field sources of dominant preimmersions
A dominant preimmersion from the spectrum of a field into an integral scheme is its generic-point morphism, up to the actual isomorphism of source schemes induced by the map on the generic stalk.
Imports3
- Mathlib.AlgebraicGeometry.FunctionField
- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
- Mathlib.AlgebraicGeometry.Stalk
Imported by6
Declarations
EtaleFundamentalGroups.dominant_field_closedPoint_eq_genericPoint
DocumentationA dominant morphism from a field spectrum sends its unique point to the generic point.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace EtaleFundamentalGroups
universe u
variable {Y : Scheme.{u}} [IsIntegral Y] {L : Type u} [Field L]
(p : Spec (.of L) ⟶ Y) [IsDominant p]
EtaleFundamentalGroups.genericFieldSourceRingEquiv
DocumentationThe generic-stalk map of a dominant preimmersion from Spec L is a field isomorphism. Surjectivity comes from the preimmersion hypothesis.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace EtaleFundamentalGroups
universe u
variable {Y : Scheme.{u}} [IsIntegral Y] {L : Type u} [Field L]
(p : Spec (.of L) ⟶ Y) [IsDominant p]
variable [IsPreimmersion p]
EtaleFundamentalGroups.genericFieldSourceIso
DocumentationA field spectrum mapping dominantly by a preimmersion is isomorphic to the spectrum of the target's function field.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace EtaleFundamentalGroups
universe u
variable {Y : Scheme.{u}} [IsIntegral Y] {L : Type u} [Field L]
(p : Spec (.of L) ⟶ Y) [IsDominant p]
variable [IsPreimmersion p]
EtaleFundamentalGroups.genericFieldSourceIso_hom_fromSpecStalk
DocumentationThe source isomorphism identifies the original morphism with the canonical generic-point morphism.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace EtaleFundamentalGroups
universe u
variable {Y : Scheme.{u}} [IsIntegral Y] {L : Type u} [Field L]
(p : Spec (.of L) ⟶ Y) [IsDominant p]
variable [IsPreimmersion p]