Module

NormalizationPushforward.lean

Nyll.SchemeTheory.Morphisms.NormalizationPushforward

2 declarations indexed from sourceView source ↗

Module documentation

The structure-sheaf pushforward of relative normalization

The section isomorphisms above affine opens of the original base imply the full structure-sheaf pushforward assertion for the native relative normalization, with no affine or Noetherian hypothesis on the base.

Imports1

Nyll.SchemeTheory.Morphisms.AffineNormalizationPushforward

Imported by3

lemma

isIso_c_of_isIso_app_affine_cover

L29 ↗

AlgebraicGeometry.isIso_c_of_isIso_app_affine_cover

Documentation

A qcqs morphism whose section maps are isomorphisms on an affine open cover induces an isomorphism of the structure sheaf with its pushforward.

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 v
variable {X S : Scheme.{u}} (f : X ⟶ S)

Lean source · statement

lemma isIso_c_of_isIso_app_affine_cover [QuasiCompact f] [QuasiSeparated f]
    {I : Type v} (U : I → S.Opens) (hU : ∀ i, IsAffineOpen (U i))
    (hCover : iSup U = ⊤) (hSections : ∀ i, IsIso (f.app (U i))) :
    IsIso f.c

lemma

isIso_toNormalization_c

L78 ↗

AlgebraicGeometry.Scheme.Hom.isIso_toNormalization_c