NYLL
Module

ConnectedCoverGenericNormalizationOpenRestriction.lean

Nyll.EtaleFundamentalGroups.Purity.ConnectedCoverGenericNormalizationOpenRestriction
2 declarations indexed from sourceView source ↗

Module documentation

The canonical normalization on the original open subscheme

The relative normalization attached to a connected finite-etale cover of an open subscheme restricts to that cover. In particular, its restriction to the range of the open immersion is finite etale.

Imports1
Imported by3

Declarations

theorem

connectedCoverGenericNormalization_restrictOpensRange_isFiniteEtale

L28 ↗
AlgebraicGeometry.FiniteEtale.connectedCoverGenericNormalization_restrictOpensRange_isFiniteEtale
Documentation

The canonical function-field normalization restricts to a finite-etale morphism on the range of the original open immersion.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem connectedCoverGenericNormalization_restrictOpensRange_isFiniteEtale
    {X U : Scheme.{u}}
    [IsIntegral U] [IsNormalIntegral U] [IsLocallyNoetherian U]
    (j : U ⟶ X) [IsOpenImmersion j] [QuasiCompact j] [QuasiSeparated j]
    (W : FiniteEtale U) [IsConnected W] :
    IsFiniteEtale
      ((connectedCoverGenericComposite W ≫ j).fromNormalization ∣_
        j.opensRange)
theorem

connectedCoverGenericNormalization_restrictOpensRange_isFiniteEtale_of_isOpenImmersion

L60 ↗
AlgebraicGeometry.FiniteEtale.connectedCoverGenericNormalization_restrictOpensRange_isFiniteEtale_of_isOpenImmersion
Documentation

Ambient normality and local Noetherianity supply the source hypotheses needed by the finite-etale open-restriction theorem.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · full declaration
theorem
    connectedCoverGenericNormalization_restrictOpensRange_isFiniteEtale_of_isOpenImmersion
    {X U : Scheme.{u}}
    [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] [QuasiCompact j] [QuasiSeparated j]
    [Nonempty U]
    (W : FiniteEtale U) [IsConnected W] :
    letI : IsIntegral U := isIntegral_of_isOpenImmersion j
    letI : IsNormalIntegral U := IsNormalIntegral.of_isOpenImmersion j
    letI : IsLocallyNoetherian U :=
      isLocallyNoetherian_of_isOpenImmersion j
    IsFiniteEtale
      ((connectedCoverGenericComposite W ≫ j).fromNormalization ∣_
        j.opensRange) := by
  let hUintegral : IsIntegral U := isIntegral_of_isOpenImmersion j
  let hUnormal : @IsNormalIntegral U hUintegral :=
    @IsNormalIntegral.of_isOpenImmersion X U _ _ hUintegral j _
  let hUnoetherian : IsLocallyNoetherian U :=
    isLocallyNoetherian_of_isOpenImmersion j
  exact
    @connectedCoverGenericNormalization_restrictOpensRange_isFiniteEtale
      X U hUintegral hUnormal hUnoetherian j _ _ _ W _

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.