Module

AffineSchemeModel.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.AffineSchemeModel

8 declarations indexed from sourceView source ↗

Module documentation

Affine Scheme Model

A finite étale cover of the literal constant extension of an affine scheme descends to an actual finite intermediate field, with its literal inclusion map.

Imports3

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.Model
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Imported by3

instance

finiteEtaleHasPullbacksAlongAffineModel

L24 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlongAffineModel

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped TensorProduct
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

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

instance

finiteEtaleStableUnderBaseChangeAlongAffineModel

L30 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleStableUnderBaseChangeAlongAffineModel

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped TensorProduct
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleHasPullbacksAlongAffineModel
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩

Lean source · statement

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

def

affineCoefficientIso

L37 ↗

AlgebraicGeometry.FiniteEtale.affineCoefficientIso

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped TensorProduct
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleHasPullbacksAlongAffineModel
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongAffineModel
    {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 affineCoefficientIso
    (k E R : Type u) [Field k] [Field E] [CommRing R]
    [Algebra k E] [Algebra k R]
    (U : Scheme.{u}) (f : U ⟶ Spec (CommRingCat.of k))
    (e : U ≅ Spec (CommRingCat.of R))
    (he : e.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap k R)) = f) :
    Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k E))) f ≅
      Spec (CommRingCat.of (R ⊗[k] E))

theorem

affineCoefficientIso_inv_fst

L51 ↗

AlgebraicGeometry.FiniteEtale.affineCoefficientIso_inv_fst

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped TensorProduct
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleHasPullbacksAlongAffineModel
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongAffineModel
    {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

theorem affineCoefficientIso_inv_fst
    (k E R : Type u) [Field k] [Field E] [CommRing R]
    [Algebra k E] [Algebra k R]
    (U : Scheme.{u}) (f : U ⟶ Spec (CommRingCat.of k))
    (e : U ≅ Spec (CommRingCat.of R))
    (he : e.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap k R)) = f) :
    (affineCoefficientIso k E R U f e he).inv ≫ Limits.pullback.fst _ _ =
      Spec.map (CommRingCat.ofHom
        (Algebra.TensorProduct.includeRight : E →ₐ[k] R ⊗[k] E).toRingHom)

theorem

affineCoefficientIso_inv_snd

L67 ↗

AlgebraicGeometry.FiniteEtale.affineCoefficientIso_inv_snd

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped TensorProduct
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleHasPullbacksAlongAffineModel
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongAffineModel
    {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

theorem affineCoefficientIso_inv_snd
    (k E R : Type u) [Field k] [Field E] [CommRing R]
    [Algebra k E] [Algebra k R]
    (U : Scheme.{u}) (f : U ⟶ Spec (CommRingCat.of k))
    (e : U ≅ Spec (CommRingCat.of R))
    (he : e.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap k R)) = f) :
    (affineCoefficientIso k E R U f e he).inv ≫ Limits.pullback.snd _ _ =
      Spec.map (CommRingCat.ofHom (algebraMap R (R ⊗[k] E))) ≫ e.inv

theorem

affine_structure_factorization

L82 ↗

AlgebraicGeometry.FiniteEtale.affine_structure_factorization

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped TensorProduct
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleHasPullbacksAlongAffineModel
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongAffineModel
    {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

theorem affine_structure_factorization
    (k : Type u) [Field k] (U : Scheme.{u}) [IsAffine U]
    (f : U ⟶ Spec (CommRingCat.of k)) :
    let _ : Algebra k Γ(U, ⊤) :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    U.isoSpec.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap k Γ(U, ⊤))) = f := by
  intro
  change U.isoSpec.hom ≫ Spec.map ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop) = f
  rw [Spec.map_comp, Scheme.isoSpec_hom_naturality_assoc,
    ← Scheme.isoSpec_Spec_inv, Iso.hom_inv_id, Category.comp_id]

theorem

affineCoefficientIso_naturality

L93 ↗

AlgebraicGeometry.FiniteEtale.affineCoefficientIso_naturality

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped TensorProduct
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleHasPullbacksAlongAffineModel
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongAffineModel
    {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

theorem affineCoefficientIso_naturality
    (k L R : Type u) [Field k] [Field L] [CommRing R]
    [Algebra k L] [Algebra k R] (F : IntermediateField k L)
    (U : Scheme.{u}) (f : U ⟶ Spec (CommRingCat.of k))
    (e : U ≅ Spec (CommRingCat.of R))
    (he : e.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap k R)) = f) :
    Limits.pullback.map
        (Spec.map (CommRingCat.ofHom (algebraMap k L))) f
        (Spec.map (CommRingCat.ofHom (algebraMap k F))) f
        (Spec.map (CommRingCat.ofHom F.val.toRingHom)) (𝟙 U) (𝟙 _)
        (by rw [Category.comp_id, ← Spec.map_comp]; rfl)
        (by rw [Category.comp_id, Category.id_comp]) ≫
      (affineCoefficientIso k F R U f e he).hom =
    (affineCoefficientIso k L R U f e he).hom ≫
      Spec.map (CommRingCat.ofHom
        (Algebra.TensorProduct.map (R := k) (S := R) (AlgHom.id R R) F.val).toRingHom) := by
  let p := Limits.pullback.map
    (Spec.map (CommRingCat.ofHom (algebraMap k L))) f
    (Spec.map (CommRingCat.ofHom (algebraMap k F))) f
    (Spec.map (CommRingCat.ofHom F.val.toRingHom)) (𝟙 U) (𝟙 _)
    (by rw [Category.comp_id, ← Spec.map_comp]; rfl)
    (by rw [Category.comp_id, Category.id_comp])
  let t := Spec.map (CommRingCat.ofHom
    (Algebra.TensorProduct.map (R := k) (S := R) (AlgHom.id R R) F.val).toRingHom)
  have hnat : (affineCoefficientIso k L R U f e he).inv ≫ p =
      t ≫ (affineCoefficientIso k F R U f e he).inv := by
    apply Limits.pullback.hom_ext
    · simp only [Category.assoc, p, Limits.pullback.map, Limits.pullback.lift_fst,
        affineCoefficientIso_inv_fst_assoc, affineCoefficientIso_inv_fst]
      dsimp only [t]
      rw [← Spec.map_comp, ← Spec.map_comp]
      apply congrArg (fun g : CommRingCat.of F ⟶ CommRingCat.of (R ⊗[k] L) => Spec.map g)
      apply CommRingCat.hom_ext
      apply RingHom.ext
      intro x
      change (1 : R) ⊗ₜ[k] F.val x =
        Algebra.TensorProduct.map (AlgHom.id R R) F.val ((1 : R) ⊗ₜ[k] x)
      rw [Algebra.TensorProduct.map_tmul, AlgHom.id_apply]
    · simp only [Category.assoc, p, Limits.pullback.map, Limits.pullback.lift_snd,
        Category.comp_id, affineCoefficientIso_inv_snd]
      dsimp only [t]
      rw [← Spec.map_comp_assoc]
      congr 2
  change p ≫ (affineCoefficientIso k F R U f e he).hom =
    (affineCoefficientIso k L R U f e he).hom ≫ t
  rw [← Iso.inv_comp_eq]
  rw [← Category.assoc, hnat, Category.assoc, Iso.inv_hom_id, Category.comp_id]

theorem

exists_finiteIntermediateField_affine_scheme_model

L143 ↗

AlgebraicGeometry.FiniteEtale.exists_finiteIntermediateField_affine_scheme_model

Documentation

A finite étale cover of the literal constant extension of an affine scheme descends to an actual finite intermediate field, with its literal inclusion map.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped TensorProduct
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleHasPullbacksAlongAffineModel
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongAffineModel
    {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

theorem exists_finiteIntermediateField_affine_scheme_model
    (k L : Type u) [Field k] [Field L] [Algebra k L] [Algebra.IsAlgebraic k L]
    (U : Scheme.{u}) [IsAffine U] (f : U ⟶ Spec (CommRingCat.of k))
    (X : FiniteEtale (Limits.pullback
      (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)) :
    ∃ F : IntermediateField k L, FiniteDimensional k F ∧
      ∃ X₀ : FiniteEtale (Limits.pullback
        (Spec.map (CommRingCat.ofHom (algebraMap k F))) f),
        Nonempty ((FiniteEtale.pullback (Limits.pullback.map
          (Spec.map (CommRingCat.ofHom (algebraMap k L))) f
          (Spec.map (CommRingCat.ofHom (algebraMap k F))) f
          (Spec.map (CommRingCat.ofHom F.val.toRingHom)) (𝟙 U) (𝟙 _)
          (by rw [Category.comp_id, ← Spec.map_comp]; rfl)
          (by rw [Category.comp_id, Category.id_comp]))).obj X₀ ≅ X) := by
  let R := Γ(U, ⊤)
  let : Algebra k R := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
  have he : U.isoSpec.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap k R)) = f :=
    affine_structure_factorization k U f
  let eL := affineCoefficientIso k L R U f U.isoSpec he
  let XT : FiniteEtale (Spec (CommRingCat.of (R ⊗[k] L))) :=
    (FiniteEtale.pullback eL.inv).obj X
  obtain ⟨F, hF, X₀, ⟨e₀⟩⟩ :=
    exists_finiteIntermediateField_affine_model k L R XT
  let eF := affineCoefficientIso k F R U f U.isoSpec he
  let p := Limits.pullback.map
    (Spec.map (CommRingCat.ofHom (algebraMap k L))) f
    (Spec.map (CommRingCat.ofHom (algebraMap k F))) f
    (Spec.map (CommRingCat.ofHom F.val.toRingHom)) (𝟙 U) (𝟙 _)
    (by rw [Category.comp_id, ← Spec.map_comp]; rfl)
    (by rw [Category.comp_id, Category.id_comp])
  let t := Spec.map (CommRingCat.ofHom
    (Algebra.TensorProduct.map (R := k) (S := R) (AlgHom.id R R) F.val).toRingHom)
  have hpt : p ≫ eF.hom = eL.hom ≫ t :=
    affineCoefficientIso_naturality k L R F U f U.isoSpec he
  let c₁ : FiniteEtale.pullback (p ≫ eF.hom) ≅
      FiniteEtale.pullback eF.hom ⋙ FiniteEtale.pullback p :=
    MorphismProperty.Over.pullbackComp (P := @IsFiniteEtale) (Q := ⊤) p eF.hom
  let c₂ : FiniteEtale.pullback (p ≫ eF.hom) ≅
      FiniteEtale.pullback (eL.hom ≫ t) :=
    MorphismProperty.Over.pullbackCongr (P := @IsFiniteEtale) (Q := ⊤) hpt
  let c₃ : FiniteEtale.pullback (eL.hom ≫ t) ≅
      FiniteEtale.pullback t ⋙ FiniteEtale.pullback eL.hom :=
    MorphismProperty.Over.pullbackComp (P := @IsFiniteEtale) (Q := ⊤) eL.hom t
  let E : FiniteEtale (Limits.pullback
      (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) ≌
      FiniteEtale (Spec (CommRingCat.of (R ⊗[k] L))) :=
    MorphismProperty.Over.pullbackIso
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ eL
  refine ⟨F, hF, (FiniteEtale.pullback eF.hom).obj X₀, ⟨?_⟩⟩
  exact (c₁.app X₀).symm ≪≫ c₂.app X₀ ≪≫ c₃.app X₀ ≪≫
    (FiniteEtale.pullback eL.hom).mapIso e₀ ≪≫ (E.unitIso.app X).symm

Module documentation

Affine Scheme Model

Declarations