NYLL
Module

Geometry.lean

Nyll.SchemeTheory.Pi1.FiniteEtale.Geometry
40 declarations indexed from sourceView source ↗

Module documentation

Geometric infrastructure for finite étale schemes

This module contains the scheme-theoretic and over-field results used by the finite étale category, independently of fundamental groups and Galois objects.

Imports23
Imported by14

Declarations

lemma

finite_primeSpectrum_of_etale_field

L76 ↗
AlgebraicGeometry.FiniteEtale.finite_primeSpectrum_of_etale_field
Documentation

An étale map whose source ring is isomorphic to a field has a finite prime spectrum.

Source context 7 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
Lean source · statement
lemma finite_primeSpectrum_of_etale_field
    {K A B : Type u} [Field K] [CommRing A] [CommRing B]
    (e : A ≃+* K) (g : A →+* B) (hg : g.Etale) :
    Finite (PrimeSpectrum B)
lemma

finite_of_isEtale_of_isAffineHom

L89 ↗
AlgebraicGeometry.FiniteEtale.finite_of_isEtale_of_isAffineHom
Source context 7 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
Lean source · statement
lemma finite_of_isEtale_of_isAffineHom (X : Scheme.{u}) {Ω : Type u} [Field Ω]
    (f : X ⟶ Spec (.of Ω)) [Etale f] [IsAffineHom f] :
    Finite X
instance

(anonymous instance)

L101 ↗
Source context 7 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
Lean source · statement
instance {Ω : Type u} [Field Ω] (X : FiniteEtale (Spec (.of Ω))) : Fintype X.left
def

forgetScheme

L112 ↗
AlgebraicGeometry.FiniteEtale.forgetScheme
Documentation

Take the finite set of points of a finite etale scheme over a field.

Source context 7 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
Lean source · full declaration
def forgetScheme (Ω : Type u) [Field Ω] : FiniteEtale (Spec (.of Ω)) ⥤ FintypeCat.{u} where
  obj X := FintypeCat.of X.left
  map {X Y} f := { hom := TypeCat.ofHom (⇑f.left : ↥X.left → ↥Y.left) }
lemma

SpecMap_iff

L118 ↗
AlgebraicGeometry.IsFiniteEtale.SpecMap_iff
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
lemma _root_.AlgebraicGeometry.IsFiniteEtale.SpecMap_iff {R S : CommRingCat.{u}}
    {f : R ⟶ S} :
    IsFiniteEtale (Spec.map f) ↔ f.hom.FiniteEtale
instance

(anonymous instance)

L126 ↗
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
instance {ι : Type u} [Finite ι] (R : Type u) [CommRing R] :
    IsFiniteEtale (Spec.map <| CommRingCat.ofHom <| algebraMap R (ι → R))
def

inventScheme

L136 ↗
AlgebraicGeometry.FiniteEtale.inventScheme
Documentation

Construct the finite etale scheme whose section ring is the ring of functions from a finite set to the field.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · full declaration
def inventScheme (Ω : Type u) [Field Ω] : FintypeCat.{u} ⥤ FiniteEtale (Spec (.of Ω)) where
  obj S :=
    mk (Spec.map <| CommRingCat.ofHom <| algebraMap Ω (S → Ω))
  map {S T} f :=
    MorphismProperty.Over.homMk
      (Spec.map <| CommRingCat.ofHom <|
        RingHom.pi (fun s ↦ Pi.evalRingHom _ (f s))) <| by
      let a : CommRingCat.of Ω ⟶ CommRingCat.of (T → Ω) :=
        CommRingCat.ofHom (algebraMap Ω (T → Ω))
      let b : CommRingCat.of (T → Ω) ⟶ CommRingCat.of (S → Ω) :=
        CommRingCat.ofHom
          (RingHom.pi (fun s ↦ Pi.evalRingHom (fun _ ↦ Ω) (f s)))
      let c : CommRingCat.of Ω ⟶ CommRingCat.of (S → Ω) :=
        CommRingCat.ofHom (algebraMap Ω (S → Ω))
      change Spec.map b ≫ Spec.map a = Spec.map c
      rw [← Spec.map_comp]
      rfl
  map_id S := by
    apply MorphismProperty.Over.Hom.ext
    change
      Spec.map
          (CommRingCat.ofHom
            (RingHom.pi (fun s ↦
              Pi.evalRingHom (fun _ ↦ Ω)
                ((𝟙 S : S ⟶ S) s)))) =
        𝟙 (Spec (CommRingCat.of (S → Ω)))
    rw [← Spec.map_id]
    congr 2
  map_comp {S T W} f g := by
    apply MorphismProperty.Over.Hom.ext
    let a : CommRingCat.of (W → Ω) ⟶ CommRingCat.of (S → Ω) :=
      CommRingCat.ofHom
        (RingHom.pi (fun s ↦ Pi.evalRingHom (fun _ ↦ Ω) ((f ≫ g) s)))
    let b : CommRingCat.of (T → Ω) ⟶ CommRingCat.of (S → Ω) :=
      CommRingCat.ofHom
        (RingHom.pi (fun s ↦ Pi.evalRingHom (fun _ ↦ Ω) (f s)))
    let c : CommRingCat.of (W → Ω) ⟶ CommRingCat.of (T → Ω) :=
      CommRingCat.ofHom
        (RingHom.pi (fun t ↦ Pi.evalRingHom (fun _ ↦ Ω) (g t)))
    change Spec.map a = Spec.map b ≫ Spec.map c
    rw [← Spec.map_comp]
    congr 2
instance

(anonymous instance)

L179 ↗
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
instance (S : FintypeCat.{u}) :
    Fintype (Spec (CommRingCat.of (S.obj → Ω))).toPresheafedSpace
def

specPiEquiv

L192 ↗
AlgebraicGeometry.FiniteEtale.specPiEquiv
Documentation

Identify the points of the spectrum of a finite product of fields with its product indices.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
def specPiEquiv (ι : Type u) [Finite ι] (K : Type u) [Field K] :
    Spec (.of (ι → K)) ≃ ι
lemma

specPiEquiv_symm_apply

L198 ↗
AlgebraicGeometry.FiniteEtale.specPiEquiv_symm_apply
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
lemma specPiEquiv_symm_apply (ι : Type u) [Finite ι] (K : Type u) [Field K]
    (i : ι) : (specPiEquiv ι K).symm i =
      (Spec.map <| CommRingCat.ofHom <| Pi.evalRingHom _ i).base default
def

inventForgetIso

L205 ↗
AlgebraicGeometry.FiniteEtale.inventForgetIso
Documentation

The points of the finite etale scheme constructed from a finite set recover that set naturally.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
def inventForgetIso : inventScheme Ω ⋙ forgetScheme Ω ≅ 𝟭 FintypeCat
instance

(anonymous instance)

L216 ↗
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
instance (X : Scheme.{u}) (R : CommRingCat.{u}) [X.Over (Spec R)] (U : X.Opens) :
    Algebra R Γ(X, U)
instance

(anonymous instance)

L223 ↗
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
instance (X : Scheme.{u}) (R : Type u) [CommRing R] [X.Over (Spec (.of R))] (U : X.Opens) :
    Algebra R Γ(X, U)
lemma

appLE_comp_algebraMap

L230 ↗
AlgebraicGeometry.FiniteEtale.appLE_comp_algebraMap
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
lemma appLE_comp_algebraMap {X Y : Scheme.{u}} (f : X ⟶ Y) (R : Type u) [CommRing R]
    [X.Over (Spec (.of R))] [Y.Over (Spec (.of R))] [f.IsOver (Spec (.of R))]
    (U : Y.Opens) (V : X.Opens) (hUV : V ≤ f ⁻¹ᵁ U) :
    (f.appLE U V hUV).hom.comp (algebraMap R Γ(Y, U)) = algebraMap R Γ(X, V)
instance

(anonymous instance)

L242 ↗
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
instance (X : Scheme.{u}) (R : Type u) [CommRing R] [X.Over (Spec (.of R))]
    [Etale (X ↘ Spec (.of R))] [IsAffineHom (X ↘ Spec (.of R))] :
    Algebra.Etale R Γ(X, ⊤)
instance

(anonymous instance)

L253 ↗
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
instance (X : Scheme.{u}) (R : Type u) [Field R] [X.Over (Spec (.of R))]
    [Etale (X ↘ Spec (.of R))] [IsAffineHom (X ↘ Spec (.of R))] :
    Module.Finite R Γ(X, ⊤)
lemma

appTop_left_comp_algebraMap

L259 ↗
AlgebraicGeometry.FiniteEtale.appTop_left_comp_algebraMap
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
lemma appTop_left_comp_algebraMap {X Y : FiniteEtale (Spec <| .of Ω)} (f : X ⟶ Y) :
    f.left.appTop.hom.comp (algebraMap Ω Γ(Y.left, ⊤)) = algebraMap Ω Γ(X.left, ⊤)
lemma

appTop_left_algebraMap

L275 ↗
AlgebraicGeometry.FiniteEtale.appTop_left_algebraMap
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
lemma appTop_left_algebraMap {X Y : FiniteEtale (Spec <| .of Ω)} (f : X ⟶ Y) (x : Ω) :
    f.left.appTop.hom (algebraMap Ω Γ(Y.left, ⊤) x) = algebraMap Ω Γ(X.left, ⊤) x
instance

(anonymous instance)

L279 ↗
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
instance {S : Scheme.{u}} (X : FiniteEtale S) : IsFiniteEtale (X.left ↘ S)
def

etaleFunctionsAlgEquiv

L285 ↗
AlgebraicGeometry.FiniteEtale.etaleFunctionsAlgEquiv
Documentation

Reindex the canonical decomposition of an étale algebra by an equivalent point type.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
def etaleFunctionsAlgEquiv (K A : Type u) [Field K] [CommRing A] [Algebra K A]
    [Algebra.Etale K A] [IsSepClosed K] {ι : Type u} (e : ι ≃ PrimeSpectrum A) :
    A ≃ₐ[K] (ι → K)
def

isoSpecFun

L293 ↗
AlgebraicGeometry.IsFiniteEtale.isoSpecFun
Documentation

A finite etale scheme over a separably closed field is the spectrum of the ring of functions on its points.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
def _root_.AlgebraicGeometry.IsFiniteEtale.isoSpecFun [IsSepClosed Ω] (X : Scheme.{u})
    [X.Over (Spec (.of Ω))] [IsFiniteEtale (X ↘ Spec (.of Ω))] :
    X ≅ Spec (.of <| X → Ω)
lemma

isoSpec_hom_comp_specMap_algebraMap

L304 ↗
AlgebraicGeometry.FiniteEtale.isoSpec_hom_comp_specMap_algebraMap
Documentation

The canonical affine presentation recovers the structure map from the scalar map.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
lemma isoSpec_hom_comp_specMap_algebraMap
    {R : Type u} [CommRing R] (X : Scheme.{u})
    [X.Over (Spec (.of R))] [IsAffine X] :
    X.isoSpec.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap R Γ(X, ⊤))) =
      X ↘ Spec (.of R)
lemma

isoSpec_hom_comp_specMap_algEquiv

L321 ↗
AlgebraicGeometry.FiniteEtale.isoSpec_hom_comp_specMap_algEquiv
Documentation

An algebra equivalence on affine global sections gives a morphism over the base ring.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
lemma isoSpec_hom_comp_specMap_algEquiv
    {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    (X : Scheme.{u}) [X.Over (Spec (.of R))] [IsAffine X]
    (e : Γ(X, ⊤) ≃ₐ[R] A) :
    X.isoSpec.hom ≫ Spec.map (CommRingCat.ofHom e.symm.toRingEquiv.toRingHom) ≫
      Spec.map (CommRingCat.ofHom (algebraMap R A)) = X ↘ Spec (.of R)
lemma

isoSpecFun_hom_SpecMap

L335 ↗
AlgebraicGeometry.IsFiniteEtale.isoSpecFun_hom_SpecMap
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
lemma _root_.AlgebraicGeometry.IsFiniteEtale.isoSpecFun_hom_SpecMap [IsSepClosed Ω]
    (X : Scheme.{u}) [X.Over (Spec (.of Ω))] [IsFiniteEtale (X ↘ Spec (.of Ω))] :
    (IsFiniteEtale.isoSpecFun Ω X).hom ≫
      Spec.map (CommRingCat.ofHom <| algebraMap Ω (X → Ω)) = X ↘ Spec (.of Ω)
instance

(anonymous instance)

L347 ↗
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
instance (priority := 900) [IsAffine X] (Y : FiniteEtale X) : IsAffine Y.left
def

forgetInventIso

L356 ↗
AlgebraicGeometry.FiniteEtale.forgetInventIso
Documentation

A finite etale scheme over a separably closed field is naturally recovered from its finite set of points.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
def forgetInventIso [IsSepClosed Ω] :
    𝟭 (FiniteEtale (Spec (.of Ω))) ≅ forgetScheme Ω ⋙ inventScheme Ω
def

equivFintypeCat

L458 ↗
AlgebraicGeometry.FiniteEtale.equivFintypeCat
Documentation

The equivalence between finite etale schemes over a separably closed field and finite sets.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
def equivFintypeCat [IsSepClosed Ω] : FiniteEtale (Spec <| .of Ω) ≌ FintypeCat.{u}
instance

(anonymous instance)

L462 ↗
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
Lean source · statement
instance [IsSepClosed Ω] : (forgetScheme Ω).IsEquivalence
def

connCompOpen

L470 ↗
AlgebraicGeometry.Scheme.connCompOpen
Documentation

The open subset corresponding to one component when the scheme has finitely many connected components.

Source context 10 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
Lean source · statement
def _root_.AlgebraicGeometry.Scheme.connCompOpen {X : Scheme.{u}}
    [Finite (_root_.ConnectedComponents X)]
    (i : _root_.ConnectedComponents X) : X.Opens
def

connectedComponents

L478 ↗
AlgebraicGeometry.Scheme.connectedComponents
Documentation

The open cover by connected components of a scheme with finitely many connected components.

Source context 10 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
Lean source · full declaration
def _root_.AlgebraicGeometry.Scheme.connectedComponents (X : Scheme.{u})
      [Finite (_root_.ConnectedComponents X)] :
    X.OpenCover where
  I₀ := _root_.ConnectedComponents X
  X c := X.connCompOpen c
  f c := (X.connCompOpen c).ι
  mem₀ := by
    rw [Scheme.ofArrows_mem_precoverage_iff]
    refine ⟨?_, ?_⟩
    · intro x
      refine ⟨.mk x, ?_⟩
      exact ⟨⟨x, rfl⟩, rfl⟩
    · infer_instance
instance

(anonymous instance)

L492 ↗
Source context 10 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
Lean source · statement
instance {X : Scheme.{u}} [Finite (_root_.ConnectedComponents X)]
    (i : _root_.ConnectedComponents X) :
    ConnectedSpace (X.connectedComponents.X i)
instance

(anonymous instance)

L501 ↗
Source context 10 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
Lean source · statement
instance {X : Scheme.{u}} [Finite (_root_.ConnectedComponents X)]
    (i : _root_.ConnectedComponents X) :
    IsClosedImmersion (X.connectedComponents.f i)
lemma

isIso_of_isIso_snd

L511 ↗
AlgebraicGeometry.IsFiniteEtale.isIso_of_isIso_snd
Source context 10 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
Lean source · statement
lemma _root_.AlgebraicGeometry.IsFiniteEtale.isIso_of_isIso_snd {X Y Z : Scheme.{u}} (f : X ⟶ Z)
    (g : Y ⟶ Z) [IsFiniteEtale f] [PreconnectedSpace Z] [Nonempty Y]
    [IsIso (pullback.snd f g)] : IsIso f
instance

(anonymous instance)

L521 ↗
Source context 10 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
Lean source · statement
instance {X Y Z : Scheme.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) [IsFiniteEtale g] :
    IsFiniteEtale (pullback.fst f g)
instance

(anonymous instance)

L533 ↗
Source context 10 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
Lean source · statement
instance {X Y Z : Scheme.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) [IsFiniteEtale f] :
    IsFiniteEtale (pullback.snd f g)
instance

surjective

L545 ↗
AlgebraicGeometry.IsFiniteEtale.surjective
Source context 10 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
Lean source · statement
instance _root_.AlgebraicGeometry.IsFiniteEtale.surjective {X Y : Scheme.{u}} (f : X ⟶ Y)
    [PreconnectedSpace Y] [Nonempty X] [IsFiniteEtale f] :
    Surjective f
lemma

isIso_of_isIso_snd'

L554 ↗
AlgebraicGeometry.IsFiniteEtale.isIso_of_isIso_snd'
Source context 10 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
Lean source · statement
lemma _root_.AlgebraicGeometry.IsFiniteEtale.isIso_of_isIso_snd' {X Y Z : Scheme.{u}} (f : X ⟶ Z)
    (g : Y ⟶ Z) [IsFiniteEtale f]
    [Finite (_root_.ConnectedComponents Z)]
    [∀ i : _root_.ConnectedComponents Z, Nonempty ↑(Limits.pullback g
      (Z.connectedComponents.f i))]
    [IsIso (pullback.snd f g)] : IsIso f
lemma

isIso_of_isIso_left

L628 ↗
AlgebraicGeometry.FiniteEtale.isIso_of_isIso_left
Source context 10 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
Lean source · statement
lemma isIso_of_isIso_left {A B : FiniteEtale X} (f : A ⟶ B) [IsIso f.left] : IsIso f
instance

(anonymous instance)

L632 ↗
Source context 10 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
Lean source · statement
instance [ConnectedSpace X] (Y : FiniteEtale X) :
    Finite (_root_.ConnectedComponents Y.left)
instance

(anonymous instance)

L641 ↗
Source context 11 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
namespace FiniteEtale
variable (X : Scheme.{u})
variable (Ω : Type u) [Field Ω]
variable {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
variable {X}
open MorphismProperty
Lean source · statement
instance {Y : Scheme.{u}} [Nonempty Y] (g : Y ⟶ X) [ConnectedSpace X] :
    (pullback g).ReflectsIsomorphisms

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