NYLL
Module

ClosedFiberBaseChange.lean

Nyll.SchemeTheory.Etale.ClosedFiberBaseChange
8 declarations indexed from sourceView source ↗

Module documentation

Actual closed fibres under a local base change

The closed fibre after a local base change is the base change of the original closed fibre along the canonical residue-field map. When the extended maximal ideal is the new maximal ideal, it is also the base change of the original closed-fibre inclusion over the original base. Both comparisons use the actual pullback maps and retain their projection equations.

Imports3
Imported by2

Declarations

lemma

residue_square

L39 ↗
AlgebraicGeometry.residue_square
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
variable [IsLocalRing A] [IsLocalRing B] [IsLocalHom (algebraMap A B)]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local notation "baseMap" => Spec.map (CommRingCat.ofHom (algebraMap A B))
local notation "residueA" => Spec.map (CommRingCat.ofHom (IsLocalRing.residue A))
local notation "residueB" => Spec.map (CommRingCat.ofHom (IsLocalRing.residue B))
local notation "residueMap" =>
  Spec.map (CommRingCat.ofHom (IsLocalRing.ResidueField.map (algebraMap A B)))
Lean source · statement
lemma residue_square : residueB ≫ baseMap = residueMap ≫ residueA
def

closedFiberBaseChangeMap

L44 ↗
AlgebraicGeometry.closedFiberBaseChangeMap
Documentation

The canonical map from the new closed fibre to the old closed fibre.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
variable [IsLocalRing A] [IsLocalRing B] [IsLocalHom (algebraMap A B)]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local notation "baseMap" => Spec.map (CommRingCat.ofHom (algebraMap A B))
local notation "residueA" => Spec.map (CommRingCat.ofHom (IsLocalRing.residue A))
local notation "residueB" => Spec.map (CommRingCat.ofHom (IsLocalRing.residue B))
local notation "residueMap" =>
  Spec.map (CommRingCat.ofHom (IsLocalRing.ResidueField.map (algebraMap A B)))
Lean source · statement
def closedFiberBaseChangeMap :
    pullback (pullback.snd f baseMap) residueB ⟶ pullback f residueA
lemma

closedFiberBaseChangeMap_fst

L53 ↗
AlgebraicGeometry.closedFiberBaseChangeMap_fst
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
variable [IsLocalRing A] [IsLocalRing B] [IsLocalHom (algebraMap A B)]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local notation "baseMap" => Spec.map (CommRingCat.ofHom (algebraMap A B))
local notation "residueA" => Spec.map (CommRingCat.ofHom (IsLocalRing.residue A))
local notation "residueB" => Spec.map (CommRingCat.ofHom (IsLocalRing.residue B))
local notation "residueMap" =>
  Spec.map (CommRingCat.ofHom (IsLocalRing.ResidueField.map (algebraMap A B)))
Lean source · statement
lemma closedFiberBaseChangeMap_fst :
    closedFiberBaseChangeMap (B := B) f ≫ pullback.fst f residueA =
      pullback.fst (pullback.snd f baseMap) residueB ≫ pullback.fst f baseMap
lemma

closedFiberBaseChangeMap_snd

L59 ↗
AlgebraicGeometry.closedFiberBaseChangeMap_snd
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
variable [IsLocalRing A] [IsLocalRing B] [IsLocalHom (algebraMap A B)]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local notation "baseMap" => Spec.map (CommRingCat.ofHom (algebraMap A B))
local notation "residueA" => Spec.map (CommRingCat.ofHom (IsLocalRing.residue A))
local notation "residueB" => Spec.map (CommRingCat.ofHom (IsLocalRing.residue B))
local notation "residueMap" =>
  Spec.map (CommRingCat.ofHom (IsLocalRing.ResidueField.map (algebraMap A B)))
Lean source · statement
lemma closedFiberBaseChangeMap_snd :
    closedFiberBaseChangeMap (B := B) f ≫ pullback.snd f residueA =
      pullback.snd (pullback.snd f baseMap) residueB ≫ residueMap
lemma

isPullback_closedFiberBaseChangeMap

L65 ↗
AlgebraicGeometry.isPullback_closedFiberBaseChangeMap
Documentation

The canonical closed-fibre comparison is cartesian over the residue fields.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
variable [IsLocalRing A] [IsLocalRing B] [IsLocalHom (algebraMap A B)]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local notation "baseMap" => Spec.map (CommRingCat.ofHom (algebraMap A B))
local notation "residueA" => Spec.map (CommRingCat.ofHom (IsLocalRing.residue A))
local notation "residueB" => Spec.map (CommRingCat.ofHom (IsLocalRing.residue B))
local notation "residueMap" =>
  Spec.map (CommRingCat.ofHom (IsLocalRing.ResidueField.map (algebraMap A B)))
Lean source · statement
lemma isPullback_closedFiberBaseChangeMap :
    IsPullback (closedFiberBaseChangeMap (B := B) f)
      (pullback.snd (pullback.snd f baseMap) residueB)
      (pullback.snd f residueA) residueMap
lemma

isPullback_closedFiberBaseChangeMap_over_base

L79 ↗
AlgebraicGeometry.isPullback_closedFiberBaseChangeMap_over_base
Documentation

If the maximal ideal extends to the new maximal ideal, the same closed fibre is the pullback of the original closed-fibre inclusion over the base.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
variable [IsLocalRing A] [IsLocalRing B] [IsLocalHom (algebraMap A B)]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local notation "baseMap" => Spec.map (CommRingCat.ofHom (algebraMap A B))
local notation "residueA" => Spec.map (CommRingCat.ofHom (IsLocalRing.residue A))
local notation "residueB" => Spec.map (CommRingCat.ofHom (IsLocalRing.residue B))
local notation "residueMap" =>
  Spec.map (CommRingCat.ofHom (IsLocalRing.ResidueField.map (algebraMap A B)))
Lean source · statement
lemma isPullback_closedFiberBaseChangeMap_over_base
    (hMaximal : (IsLocalRing.maximalIdeal A).map (algebraMap A B) =
      IsLocalRing.maximalIdeal B) :
    IsPullback (closedFiberBaseChangeMap (B := B) f)
      (pullback.snd (pullback.snd f baseMap) residueB ≫ residueB)
      (pullback.fst f residueA ≫ f) baseMap
def

closedFiberBaseChangeIso

L95 ↗
AlgebraicGeometry.closedFiberBaseChangeIso
Documentation

The explicit identification with the base change of the closed-fibre inclusion.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
variable [IsLocalRing A] [IsLocalRing B] [IsLocalHom (algebraMap A B)]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local notation "baseMap" => Spec.map (CommRingCat.ofHom (algebraMap A B))
local notation "residueA" => Spec.map (CommRingCat.ofHom (IsLocalRing.residue A))
local notation "residueB" => Spec.map (CommRingCat.ofHom (IsLocalRing.residue B))
local notation "residueMap" =>
  Spec.map (CommRingCat.ofHom (IsLocalRing.ResidueField.map (algebraMap A B)))
Lean source · statement
def closedFiberBaseChangeIso
    (hMaximal : (IsLocalRing.maximalIdeal A).map (algebraMap A B) =
      IsLocalRing.maximalIdeal B) :
    pullback (pullback.snd f baseMap) residueB ≅
      pullback (pullback.fst f residueA ≫ f) baseMap
lemma

closedFiberBaseChangeIso_hom_baseChange

L104 ↗
AlgebraicGeometry.closedFiberBaseChangeIso_hom_baseChange
Documentation

Under the explicit comparison, the base change of the old closed-fibre inclusion is exactly the new closed-fibre inclusion.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
variable [IsLocalRing A] [IsLocalRing B] [IsLocalHom (algebraMap A B)]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local notation "baseMap" => Spec.map (CommRingCat.ofHom (algebraMap A B))
local notation "residueA" => Spec.map (CommRingCat.ofHom (IsLocalRing.residue A))
local notation "residueB" => Spec.map (CommRingCat.ofHom (IsLocalRing.residue B))
local notation "residueMap" =>
  Spec.map (CommRingCat.ofHom (IsLocalRing.ResidueField.map (algebraMap A B)))
Lean source · statement
lemma closedFiberBaseChangeIso_hom_baseChange
    (hMaximal : (IsLocalRing.maximalIdeal A).map (algebraMap A B) =
      IsLocalRing.maximalIdeal B) :
    (closedFiberBaseChangeIso (B := B) f hMaximal).hom ≫
      pullback.map (pullback.fst f residueA ≫ f) baseMap f baseMap
        (pullback.fst f residueA) (𝟙 _) (𝟙 _)
        (Category.comp_id _) ((Category.comp_id _).trans (Category.id_comp _).symm) =
      pullback.fst (pullback.snd f baseMap) residueB

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