ModuleAffineNormalizationPushforward.lean
Nyll.SchemeTheory.Morphisms.AffineNormalizationPushforward
3 declarations indexed from sourceView source ↗ Module documentation
Structure-sheaf pushforward for affine relative normalization
For a qcqs morphism to an affine scheme, an isomorphism on global sections extends to an isomorphism of the structure sheaf with its pushforward. Flat base change supplies the assertion on affine opens, and the sheaf basis criterion supplies it on all opens. Applied to the section isomorphism of a universally closed normalization, this proves the pushforward assertion for the actual normalization map over an affine base.
Declarations
AlgebraicGeometry.isIso_app_of_isIso_appTop
DocumentationFor a qcqs morphism to an affine scheme, a global-sections isomorphism remains an isomorphism on every affine target open.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
variable {X S : Scheme.{u}} (f : X ⟶ S)
AlgebraicGeometry.isIso_c_of_isIso_appTop
DocumentationAffine-local flat base change and the sheaf basis criterion extend the global-sections isomorphism of a qcqs morphism to its full sheaf map.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
variable {X S : Scheme.{u}} (f : X ⟶ S)
AlgebraicGeometry.Scheme.Hom.isIso_toNormalization_c_of_universallyClosed
DocumentationOver an affine base, the canonical normalization of a universally closed qcqs morphism has the same structure sheaf as the pushforward of the source.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
variable {X S : Scheme.{u}} (f : X ⟶ S)
namespace Scheme.Hom