Module

DominantPreimmersionPullback.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.DominantPreimmersionPullback

5 declarations indexed from sourceView source ↗

Module documentation

Finite-etale pullback along dominant preimmersions

A dominant quasi-compact preimmersion from a connected scheme into a normal integral scheme preserves connected finite-etale covers. If the original cover is a Galois object, faithfulness of pullback and invariance of the finite-etale rank show that the pulled-back connected cover is again Galois.

Imports5

Nyll.EtaleFundamentalGroups.FiniteEtale.Integral
Nyll.EtaleFundamentalGroups.GaloisCovers.Basic
Nyll.SchemeTheory.FiniteEtale.DensePullback
Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Imported by5

theorem

irreducibleSpace_of_isPreimmersion_of_isDominant

L34 ↗

AlgebraicGeometry.irreducibleSpace_of_isPreimmersion_of_isDominant

Documentation

A dominant preimmersion into an irreducible scheme has irreducible source.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MorphismProperty
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem irreducibleSpace_of_isPreimmersion_of_isDominant
    {U X : Scheme.{u}} (f : U ⟶ X)
    [IsPreimmersion f] [IsDominant f] [IrreducibleSpace X] :
    IrreducibleSpace U

instance

preimmersionStableUnderBaseChangeAlongDominant

L69 ↗

AlgebraicGeometry.FiniteEtale.preimmersionStableUnderBaseChangeAlongDominant

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits MorphismProperty
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u
namespace FiniteEtale

Lean source · statement

instance preimmersionStableUnderBaseChangeAlongDominant
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsPreimmersion : MorphismProperty Scheme.{u}) f

instance

quasiCompactStableUnderBaseChangeAlongDominant

L76 ↗

AlgebraicGeometry.FiniteEtale.quasiCompactStableUnderBaseChangeAlongDominant

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits MorphismProperty
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u
namespace FiniteEtale
local instance preimmersionStableUnderBaseChangeAlongDominant
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsPreimmersion : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsPreimmersion : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

instance quasiCompactStableUnderBaseChangeAlongDominant
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@QuasiCompact : MorphismProperty Scheme.{u}) f

theorem

pullback_obj_isConnected_of_isPreimmersion_of_isDominant

L86 ↗

AlgebraicGeometry.FiniteEtale.pullback_obj_isConnected_of_isPreimmersion_of_isDominant

Documentation

A dominant quasi-compact preimmersion from a connected scheme into a normal integral base preserves connectedness of connected finite-etale covers.

Source context 8 commands

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

noncomputable section
open CategoryTheory Limits MorphismProperty
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u
namespace FiniteEtale
local instance preimmersionStableUnderBaseChangeAlongDominant
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsPreimmersion : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsPreimmersion : MorphismProperty Scheme.{u})) h hf⟩
local instance quasiCompactStableUnderBaseChangeAlongDominant
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@QuasiCompact : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@QuasiCompact : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

theorem pullback_obj_isConnected_of_isPreimmersion_of_isDominant
    {U X : Scheme.{u}}
    [IsIntegral X] [IsNormalIntegral X]
    [ConnectedSpace U]
    (j : U ⟶ X) [hjpre : IsPreimmersion j]
    [hjdom : IsDominant j] [hjqc : QuasiCompact j]
    (W : FiniteEtale X) [IsConnected W] :
    IsConnected ((pullback j).obj W)

theorem

pullback_obj_isGalois_of_isPreimmersion_of_isDominant

L122 ↗

AlgebraicGeometry.FiniteEtale.pullback_obj_isGalois_of_isPreimmersion_of_isDominant

Documentation

Under the same dense-preimmersion hypotheses, pullback preserves categorical Galois covers.

Source context 8 commands

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

noncomputable section
open CategoryTheory Limits MorphismProperty
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u
namespace FiniteEtale
local instance preimmersionStableUnderBaseChangeAlongDominant
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsPreimmersion : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsPreimmersion : MorphismProperty Scheme.{u})) h hf⟩
local instance quasiCompactStableUnderBaseChangeAlongDominant
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@QuasiCompact : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@QuasiCompact : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

theorem pullback_obj_isGalois_of_isPreimmersion_of_isDominant
    {U X : Scheme.{u}}
    [IsIntegral X] [IsNormalIntegral X]
    [ConnectedSpace U]
    (j : U ⟶ X) [hjpre : IsPreimmersion j]
    [hjdom : IsDominant j] [hjqc : QuasiCompact j]
    (W : FiniteEtale X) (hW : IsGalois W) :
    IsGalois ((pullback j).obj W)

Module documentation

Finite-etale pullback along dominant preimmersions

Declarations

irreducibleSpace_of_isPreimmersion_of_isDominant

preimmersionStableUnderBaseChangeAlongDominant

quasiCompactStableUnderBaseChangeAlongDominant

pullback_obj_isConnected_of_isPreimmersion_of_isDominant

pullback_obj_isGalois_of_isPreimmersion_of_isDominant