Module

Basic.lean

Nyll.SchemeTheory.Pi1.FiniteEtale.Basic

44 declarations indexed from sourceView source ↗

Module documentation

Finite étale morphisms

We say a morphism is finite étale if it is finite and étale. The category FiniteEtale X is the category of finite etale schemes over X.

Imports7

Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Mathlib.CategoryTheory.Limits.MorphismProperty
Nyll.SchemeTheory.Pi1.Morphisms.Finite
Nyll.SchemeTheory.Pi1.Etale.RingHom
Nyll.SchemeTheory.Pi1.Affine.Property
Nyll.SchemeTheory.Pi1.FiniteEtale.Algebra.Splitting

Imported by87

def

FiniteEtale

L56 ↗

RingHom.FiniteEtale

Documentation

A ring homomorphism is finite étale if the induced algebra is finite étale.

Source context 5 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace RingHom

Lean source · statement

def FiniteEtale {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : Prop

lemma

finiteEtale_algebraMap_iff

L60 ↗

RingHom.finiteEtale_algebraMap_iff

Source context 5 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace RingHom

Lean source · statement

lemma finiteEtale_algebraMap_iff {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] :
    (algebraMap R S).FiniteEtale ↔ Algebra.FiniteEtale R S

lemma

iff_finite_and_etale

L68 ↗

RingHom.FiniteEtale.iff_finite_and_etale

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace RingHom
namespace FiniteEtale

Lean source · statement

lemma iff_finite_and_etale
    {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) :
    f.FiniteEtale ↔ f.Etale ∧ f.Finite

lemma

eq_and

L74 ↗

RingHom.FiniteEtale.eq_and

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace RingHom
namespace FiniteEtale

Lean source · full declaration

lemma eq_and :
    @FiniteEtale = (fun R S (_ : CommRing R) (_ : CommRing S) f ↦ f.Etale ∧ f.Finite) := by
  ext
  rw [iff_finite_and_etale]

lemma

isStableUnderBaseChange

L79 ↗

RingHom.FiniteEtale.isStableUnderBaseChange

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace RingHom
namespace FiniteEtale

Lean source · statement

lemma isStableUnderBaseChange : IsStableUnderBaseChange FiniteEtale

lemma

respectsIso

L83 ↗

RingHom.FiniteEtale.respectsIso

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace RingHom
namespace FiniteEtale

Lean source · statement

lemma respectsIso : RespectsIso FiniteEtale

lemma

hasFiniteProducts

L87 ↗

RingHom.FiniteEtale.hasFiniteProducts

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace RingHom
namespace FiniteEtale

Lean source · statement

lemma hasFiniteProducts : HasFiniteProducts FiniteEtale

lemma

hasEqualizers

L92 ↗

RingHom.FiniteEtale.hasEqualizers

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace RingHom
namespace FiniteEtale

Lean source · statement

lemma hasEqualizers : HasEqualizers FiniteEtale

lemma

hasStableEqualizers

L97 ↗

RingHom.FiniteEtale.hasStableEqualizers

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace RingHom
namespace FiniteEtale

Lean source · statement

lemma hasStableEqualizers : HasStableEqualizers FiniteEtale

instance

(anonymous instance)

L102 ↗

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace RingHom
namespace FiniteEtale

Lean source · statement

instance : (toMorphismProperty RingHom.FiniteEtale).IsStableUnderCobaseChange

class

IsFiniteEtale

L114 ↗

AlgebraicGeometry.IsFiniteEtale

Documentation

A morphism is finite étale if it is finite and étale.

Source context 5 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry

Lean source · full declaration

class IsFiniteEtale {X Y : Scheme.{u}} (f : X ⟶ Y) : Prop
  extends IsFinite f, Etale f

lemma

eq_inf

L121 ↗

AlgebraicGeometry.IsFiniteEtale.eq_inf

Source context 7 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace IsFiniteEtale
open MorphismProperty

Lean source · full declaration

lemma eq_inf :
    (@IsFiniteEtale : MorphismProperty Scheme.{u}) =
      (show MorphismProperty Scheme.{u} from
        (@IsFinite : MorphismProperty Scheme.{u}) ⊓
          (@Etale : MorphismProperty Scheme.{u})) := by
  ext f
  rw [isFiniteEtale_iff]
  rfl

instance

(anonymous instance)

L130 ↗

Source context 7 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace IsFiniteEtale
open MorphismProperty

Lean source · full declaration

instance : ContainsIdentities
    (@IsFiniteEtale : MorphismProperty Scheme.{u}) where
  id_mem X := @IsFiniteEtale.mk _ _ _
    (by infer_instance) (by infer_instance)

instance

(anonymous instance)

L135 ↗

Source context 7 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace IsFiniteEtale
open MorphismProperty

Lean source · full declaration

instance : IsStableUnderComposition
    (@IsFiniteEtale : MorphismProperty Scheme.{u}) where
  comp_mem f g hf hg := by
    let _ : IsFinite f := hf.toIsFinite
    let _ : IsFinite g := hg.toIsFinite
    let _ : Etale f := hf.toEtale
    let _ : Etale g := hg.toEtale
    exact @IsFiniteEtale.mk _ _ _ inferInstance inferInstance

instance

(anonymous instance)

L144 ↗

Source context 7 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace IsFiniteEtale
open MorphismProperty

Lean source · full declaration

instance : IsMultiplicative
    (@IsFiniteEtale : MorphismProperty Scheme.{u}) where

instance

(anonymous instance)

L147 ↗

Source context 7 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace IsFiniteEtale
open MorphismProperty

Lean source · full declaration

instance : IsStableUnderBaseChange
    (@IsFiniteEtale : MorphismProperty Scheme.{u}) where
  of_isPullback h hg := @IsFiniteEtale.mk _ _ _
    (MorphismProperty.of_isPullback
      (P := (@IsFinite : MorphismProperty Scheme.{u})) h hg.toIsFinite)
    (MorphismProperty.of_isPullback
      (P := (@Etale : MorphismProperty Scheme.{u})) h hg.toEtale)

instance

(anonymous instance)

L155 ↗

Source context 7 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace IsFiniteEtale
open MorphismProperty

Lean source · full declaration

instance : HasOfPostcompProperty
    (@IsFiniteEtale : MorphismProperty Scheme.{u})
    (@IsFiniteEtale : MorphismProperty Scheme.{u}) where
  of_postcomp f g hg hfg := @IsFiniteEtale.mk _ _ _
    (MorphismProperty.of_postcomp
      (@IsFinite : MorphismProperty Scheme.{u}) f g hg.toIsFinite hfg.toIsFinite)
    (MorphismProperty.of_postcomp
      (@Etale : MorphismProperty Scheme.{u}) f g hg.toEtale hfg.toEtale)

instance

(anonymous instance)

L164 ↗

Source context 7 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace IsFiniteEtale
open MorphismProperty

Lean source · statement

instance : HasAffineProperty
    (@IsFiniteEtale : MorphismProperty Scheme.{u})
    (affineAnd RingHom.FiniteEtale)

instance

(anonymous instance)

L255 ↗

Source context 7 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace IsFiniteEtale
open MorphismProperty

Lean source · full declaration

instance {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsFiniteEtale f] [IsFiniteEtale g] :
    IsFiniteEtale (f ≫ g) where

lemma

mono_iff

L258 ↗

AlgebraicGeometry.IsFiniteEtale.mono_iff

Source context 7 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace IsFiniteEtale
open MorphismProperty

Lean source · statement

lemma mono_iff {X Y : Scheme.{u}} (f : X ⟶ Y) [IsFiniteEtale f] :
    Mono f ↔ IsOpenImmersion f ∧ IsClosedImmersion f

def

FiniteEtale

L267 ↗

AlgebraicGeometry.FiniteEtale

Documentation

The category of schemes finite étale over X.

Source context 5 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry

Lean source · statement

def FiniteEtale (X : Scheme.{u}) : Type _

instance

(anonymous instance)

L276 ↗

Source context 7 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})

Lean source · statement

instance : Category (FiniteEtale X)

instance

finiteEtaleOverCategory

L282 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleOverCategory

Source context 7 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})

Lean source · statement

instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X)

instance

finiteEtaleHasPullbacksAlong

L288 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlong

Source context 8 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X

Lean source · statement

instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f

instance

finiteEtaleIsStableUnderBaseChangeAlong

L294 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleIsStableUnderBaseChangeAlong

Source context 9 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩

Lean source · statement

instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f

def

forget

L302 ↗

AlgebraicGeometry.FiniteEtale.forget

Documentation

The forgetful functor from schemes finite étale over X to schemes over X.

Source context 10 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

def forget : FiniteEtale X ⥤ Over X

def

forgetFullyFaithful

L309 ↗

AlgebraicGeometry.FiniteEtale.forgetFullyFaithful

Documentation

The forgetful functor from schemes finite étale over X to schemes over X is fully faithful.

Source context 10 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

def forgetFullyFaithful : (FiniteEtale.forget X).FullyFaithful

instance

(anonymous instance)

L314 ↗

Source context 10 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

instance : (FiniteEtale.forget X).Full

instance

(anonymous instance)

L316 ↗

Source context 10 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

instance : (FiniteEtale.forget X).Faithful

instance

(anonymous instance)

L319 ↗

Source context 10 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

instance : HasTerminal (FiniteEtale X)

instance

(anonymous instance)

L323 ↗

Source context 10 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

instance : HasPullbacks (FiniteEtale X)

instance

(anonymous instance)

L327 ↗

Source context 10 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

instance (f : FiniteEtale X) : IsFiniteEtale f.hom

def

toAffine

L330 ↗

AlgebraicGeometry.FiniteEtale.toAffine

Documentation

The forgetful functor to the category of schemes affine over X.

Source context 10 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · full declaration

def toAffine : FiniteEtale X ⥤ Affine X where
  obj f := ⟨f.toComma, inferInstance⟩
  map {X Y} f := ⟨f.toCommaMorphism, trivial, trivial⟩

def

toAffineFullyFaithful

L335 ↗

AlgebraicGeometry.FiniteEtale.toAffineFullyFaithful

Documentation

The fully faithful embedding of finite étale schemes over X into affine schemes over X.

Source context 10 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · full declaration

def toAffineFullyFaithful : (toAffine X).FullyFaithful where
  preimage f := ⟨f.toCommaMorphism, trivial, trivial⟩

instance

(anonymous instance)

L338 ↗

Source context 10 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

instance : (toAffine X).Faithful

instance

(anonymous instance)

L339 ↗

Source context 10 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

instance : (toAffine X).Full

instance

(anonymous instance)

L341 ↗

Source context 10 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

instance : HasFiniteColimits (FiniteEtale X)

instance

(anonymous instance)

L348 ↗

Source context 10 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

instance (f g : FiniteEtale X) (i : f ⟶ g) : IsFiniteEtale i.hom.left

lemma

mono_iff

L356 ↗

AlgebraicGeometry.FiniteEtale.mono_iff

Source context 10 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

lemma mono_iff (f g : FiniteEtale X) (i : f ⟶ g) :
    Mono i ↔ IsOpenImmersion i.hom.left ∧ IsClosedImmersion i.hom.left

abbrev

pullback

L379 ↗

AlgebraicGeometry.FiniteEtale.pullback

Documentation

Base change of finite étale schemes along f.

Source context 11 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X}

Lean source · statement

abbrev pullback {Y : Scheme.{u}} (f : X ⟶ Y) : FiniteEtale Y ⥤ FiniteEtale X

def

mk

L385 ↗

AlgebraicGeometry.FiniteEtale.mk

Documentation

A finite étale morphism f : T ⟶ X viewed as an object of FiniteEtale X.

Source context 11 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X}

Lean source · statement

def mk {T : Scheme.{u}} (f : T ⟶ X) [IsFiniteEtale f] : FiniteEtale X

lemma

mk_hom

L391 ↗

AlgebraicGeometry.FiniteEtale.mk_hom

Source context 11 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X}

Lean source · statement

lemma mk_hom {T : Scheme.{u}} (f : T ⟶ X) [IsFiniteEtale f] : (mk f).hom = f

lemma

mk_left

L394 ↗

AlgebraicGeometry.FiniteEtale.mk_left

Source context 11 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X}

Lean source · statement

lemma mk_left {T : Scheme.{u}} (f : T ⟶ X) [IsFiniteEtale f] : (mk f).left = T

instance

(anonymous instance)

L397 ↗

Source context 12 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
local instance finiteEtaleOverCategory (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X}
open RingHom in

Lean source · statement

instance {Y : Scheme.{u}} (f : X ⟶ Y) :
    PreservesFiniteColimits (pullback f)

Module documentation

Finite étale morphisms

Declarations