NYLL
Module

CompactificationBoundary.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.CompactificationBoundary
7 declarations indexed from sourceView source ↗

Module documentation

The actual normalization compactification and its boundary

The original connected finite étale cover embeds openly in the normalization of the ambient proper scheme in its own function field. Its complement is exactly the inverse image of the original boundary. No extension across the boundary is assumed to be étale.

Imports2
Imported by2

Declarations

def

connectedCoverCompactificationInclusion

L36 ↗
AlgebraicGeometry.FiniteEtale.connectedCoverCompactificationInclusion
Documentation

The original cover as an open subscheme of the actual normalization.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
universe u
variable {X U : Scheme.{u}}
  [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
  [IsIntegral U] [IsNormalIntegral U] [IsLocallyNoetherian U]
  (j : U ⟶ X) [IsOpenImmersion j] [QuasiCompact j] [QuasiSeparated j]
  (W : FiniteEtale U) [IsConnected W]
Lean source · statement
def connectedCoverCompactificationInclusion :
    W.left ⟶ (connectedCoverGenericComposite W ≫ j).normalization
instance

connectedCoverCompactificationInclusion_isOpenImmersion

L41 ↗
AlgebraicGeometry.FiniteEtale.connectedCoverCompactificationInclusion_isOpenImmersion
Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
universe u
variable {X U : Scheme.{u}}
  [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
  [IsIntegral U] [IsNormalIntegral U] [IsLocallyNoetherian U]
  (j : U ⟶ X) [IsOpenImmersion j] [QuasiCompact j] [QuasiSeparated j]
  (W : FiniteEtale U) [IsConnected W]
Lean source · statement
instance connectedCoverCompactificationInclusion_isOpenImmersion :
    IsOpenImmersion (connectedCoverCompactificationInclusion j W)
theorem

connectedCoverCompactificationInclusion_comp

L48 ↗
AlgebraicGeometry.FiniteEtale.connectedCoverCompactificationInclusion_comp
Documentation

The compactification inclusion commutes with the original covering map.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
universe u
variable {X U : Scheme.{u}}
  [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
  [IsIntegral U] [IsNormalIntegral U] [IsLocallyNoetherian U]
  (j : U ⟶ X) [IsOpenImmersion j] [QuasiCompact j] [QuasiSeparated j]
  (W : FiniteEtale U) [IsConnected W]
omit [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X] in
Lean source · statement
theorem connectedCoverCompactificationInclusion_comp :
    connectedCoverCompactificationInclusion j W ≫
        (connectedCoverGenericComposite W ≫ j).fromNormalization =
      W.hom ≫ j
theorem

range_connectedCoverCompactificationInclusion

L58 ↗
AlgebraicGeometry.FiniteEtale.range_connectedCoverCompactificationInclusion
Documentation

This is the equality of the actual underlying open subsets.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
universe u
variable {X U : Scheme.{u}}
  [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
  [IsIntegral U] [IsNormalIntegral U] [IsLocallyNoetherian U]
  (j : U ⟶ X) [IsOpenImmersion j] [QuasiCompact j] [QuasiSeparated j]
  (W : FiniteEtale U) [IsConnected W]
omit [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X] in
Lean source · statement
theorem range_connectedCoverCompactificationInclusion :
    Set.range (connectedCoverCompactificationInclusion j W) =
      (connectedCoverGenericComposite W ≫ j).fromNormalization ⁻¹' Set.range j
theorem

not_mem_range_connectedCoverCompactificationInclusion

L76 ↗
AlgebraicGeometry.FiniteEtale.not_mem_range_connectedCoverCompactificationInclusion
Documentation

Boundary membership is computed by the original boundary, with the original cover recovered on its full inverse image.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
universe u
variable {X U : Scheme.{u}}
  [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
  [IsIntegral U] [IsNormalIntegral U] [IsLocallyNoetherian U]
  (j : U ⟶ X) [IsOpenImmersion j] [QuasiCompact j] [QuasiSeparated j]
  (W : FiniteEtale U) [IsConnected W]
omit [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X] in
Lean source · statement
theorem not_mem_range_connectedCoverCompactificationInclusion
    (y : (connectedCoverGenericComposite W ≫ j).normalization) :
    y ∉ Set.range (connectedCoverCompactificationInclusion j W) ↔
      (connectedCoverGenericComposite W ≫ j).fromNormalization y ∉ Set.range j
theorem

connectedCoverCompactification_isFinite

L85 ↗
AlgebraicGeometry.FiniteEtale.connectedCoverCompactification_isFinite
Documentation

The normalization compactification is genuinely finite over the ambient scheme, from the finite separable generic extension.

Source context 6 commands

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

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

connectedCoverCompactification_isProper

L91 ↗
AlgebraicGeometry.FiniteEtale.connectedCoverCompactification_isProper
Documentation

A proper ambient scheme gives an actual proper compactification of the original finite étale cover.

Source context 6 commands

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

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

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