Module

FiniteNormalFieldSource.lean

Nyll.EtaleFundamentalGroups.Normalization.FiniteNormalFieldSource

4 declarations indexed from sourceView source ↗

Module documentation

Actual finite normal models from a specified generic field source

Imports3

Imported by2

theorem

genericFieldSourceIso_hom_genericComposite

L27 ↗

EtaleFundamentalGroups.genericFieldSourceIso_hom_genericComposite

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 {X Y : Scheme.{u}} [IsIntegral Y] [IsNormalIntegral Y]
  (f : Y ⟶ X) [IsFinite f]
  {L : Type u} [Field L] (p : Spec (.of L) ⟶ Y)
  [IsDominant p] [IsPreimmersion p] [QuasiCompact p] [QuasiSeparated p]
omit [IsNormalIntegral Y] [IsFinite f] [QuasiCompact p] [QuasiSeparated p] in

Lean source · statement

theorem genericFieldSourceIso_hom_genericComposite :
    (genericFieldSourceIso p).hom ≫
      (Y.genericExtensionMorphism Y.functionField ≫ f) = p ≫ f

def

finiteNormalFieldSourceIso

L36 ↗

EtaleFundamentalGroups.finiteNormalFieldSourceIso

Documentation

The normalization in the specified generic field is the actual finite normal source, compatibly with its original map to the base.

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 {X Y : Scheme.{u}} [IsIntegral Y] [IsNormalIntegral Y]
  (f : Y ⟶ X) [IsFinite f]
  {L : Type u} [Field L] (p : Spec (.of L) ⟶ Y)
  [IsDominant p] [IsPreimmersion p] [QuasiCompact p] [QuasiSeparated p]

Lean source · statement

def finiteNormalFieldSourceIso : (p ≫ f).normalization ≅ Y

theorem

finiteNormalFieldSourceIso_hom_fromNormalization

L43 ↗

EtaleFundamentalGroups.finiteNormalFieldSourceIso_hom_fromNormalization

Documentation

The forward isomorphism commutes with the specified finite morphism.

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 {X Y : Scheme.{u}} [IsIntegral Y] [IsNormalIntegral Y]
  (f : Y ⟶ X) [IsFinite f]
  {L : Type u} [Field L] (p : Spec (.of L) ⟶ Y)
  [IsDominant p] [IsPreimmersion p] [QuasiCompact p] [QuasiSeparated p]

Lean source · statement

theorem finiteNormalFieldSourceIso_hom_fromNormalization :
    (finiteNormalFieldSourceIso f p).hom ≫ f = (p ≫ f).fromNormalization

theorem

finiteNormalFieldSourceIso_inv_comp

L56 ↗

EtaleFundamentalGroups.finiteNormalFieldSourceIso_inv_comp

Documentation

The inverse isomorphism recovers the specified finite morphism.

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 {X Y : Scheme.{u}} [IsIntegral Y] [IsNormalIntegral Y]
  (f : Y ⟶ X) [IsFinite f]
  {L : Type u} [Field L] (p : Spec (.of L) ⟶ Y)
  [IsDominant p] [IsPreimmersion p] [QuasiCompact p] [QuasiSeparated p]

Lean source · statement

theorem finiteNormalFieldSourceIso_inv_comp :
    (finiteNormalFieldSourceIso f p).inv ≫ (p ≫ f).fromNormalization = f

Module documentation

Actual finite normal models from a specified generic field source

Declarations

genericFieldSourceIso_hom_genericComposite

finiteNormalFieldSourceIso

finiteNormalFieldSourceIso_hom_fromNormalization

finiteNormalFieldSourceIso_inv_comp