Module

StalkBaseChange.lean

Nyll.SchemeTheory.Affine.StalkBaseChange

26 declarations indexed from sourceView source ↗

Module documentation

mem map maximal Ideal of stalk Map mem map maximal Ideal of iso pullback

Imports11

Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.AlgebraicGeometry.ResidueField
Mathlib.AlgebraicGeometry.Stalk
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.AlgebraicGeometry.StructureSheaf
Mathlib.RingTheory.LocalRing.ResidueField.Basic
Mathlib.RingTheory.LocalRing.RingHom.Basic
Mathlib.RingTheory.Ideal.Maps
Mathlib.Topology.Sheaves.Stalks
Mathlib.Tactic.ByContra
Mathlib.Tactic.Ext

Imported by1

Nyll.SchemeTheory.Affine.All

lemma

residueFieldMap_bijective

L45 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.residueFieldMap_bijective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section algebra
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]
  (ι₁ : A₁ →+* A) [IsLocalHom ι₁]

Lean source · statement

lemma residueFieldMap_bijective (hres₁ : Function.Surjective ((residue A).comp ι₁)) :
  Function.Bijective (ResidueField.map ι₁)

def

resEquiv

L52 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.resEquiv

Documentation

The residue field equivalence induced by the surjective residue map.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section algebra
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]
  (ι₁ : A₁ →+* A) [IsLocalHom ι₁]

Lean source · statement

def resEquiv (hres₁ : Function.Surjective ((residue A).comp ι₁)) :
    ResidueField A₁ ≃+* ResidueField A

lemma

resEquiv_symm_residue

L56 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.resEquiv_symm_residue

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section algebra
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]
  (ι₁ : A₁ →+* A) [IsLocalHom ι₁]

Lean source · statement

lemma resEquiv_symm_residue (hres₁ : Function.Surjective ((residue A).comp ι₁)) (a₁ : A₁) :
    (resEquiv ι₁ hres₁).symm (residue A (ι₁ a₁)) = residue A₁ a₁

def

lift₁

L66 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.lift₁

Documentation

The residue field map into the quotient by the image of the maximal ideal.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section algebra
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]
  (ι₁ : A₁ →+* A) [IsLocalHom ι₁]
variable (hres₁ : Function.Surjective ((residue A).comp ι₁)) {R : Type u} [CommRing R] (b : A₁ →+*
  R)

Lean source · statement

def lift₁ : ResidueField A₁ →+* R ⧸ Ideal.map b (maximalIdeal A₁)

lemma

lift₁_residue

L72 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.lift₁_residue

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section algebra
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]
  (ι₁ : A₁ →+* A) [IsLocalHom ι₁]
variable (hres₁ : Function.Surjective ((residue A).comp ι₁)) {R : Type u} [CommRing R] (b : A₁ →+*
  R)

Lean source · statement

lemma lift₁_residue (a₁ : A₁) :
    lift₁ b (residue A₁ a₁) = Ideal.Quotient.mk (Ideal.map b (maximalIdeal A₁)) (b a₁)

def

aR

L76 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.aR

Documentation

The map from the larger local ring into the quotient, using the residue field equivalence.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section algebra
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]
  (ι₁ : A₁ →+* A) [IsLocalHom ι₁]
variable (hres₁ : Function.Surjective ((residue A).comp ι₁)) {R : Type u} [CommRing R] (b : A₁ →+*
  R)

Lean source · statement

def aR : A →+* R ⧸ Ideal.map b (maximalIdeal A₁)

lemma

aR_apply

L79 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.aR_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section algebra
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]
  (ι₁ : A₁ →+* A) [IsLocalHom ι₁]
variable (hres₁ : Function.Surjective ((residue A).comp ι₁)) {R : Type u} [CommRing R] (b : A₁ →+*
  R)

Lean source · statement

lemma aR_apply (t : A) : aR ι₁ hres₁ b t = lift₁ b ((resEquiv ι₁ hres₁).symm (residue A t))

lemma

aR_ι₁

L81 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.aR_ι₁

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section algebra
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]
  (ι₁ : A₁ →+* A) [IsLocalHom ι₁]
variable (hres₁ : Function.Surjective ((residue A).comp ι₁)) {R : Type u} [CommRing R] (b : A₁ →+*
  R)

Lean source · statement

lemma aR_ι₁ (a₁ : A₁) :
    aR ι₁ hres₁ b (ι₁ a₁) = Ideal.Quotient.mk (Ideal.map b (maximalIdeal A₁)) (b a₁)

lemma

aR_comp_ι₁

L85 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.aR_comp_ι₁

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section algebra
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]
  (ι₁ : A₁ →+* A) [IsLocalHom ι₁]
variable (hres₁ : Function.Surjective ((residue A).comp ι₁)) {R : Type u} [CommRing R] (b : A₁ →+*
  R)

Lean source · statement

lemma aR_comp_ι₁ : (aR ι₁ hres₁ b).comp ι₁ = (Ideal.Quotient.mk (Ideal.map b (maximalIdeal
  A₁))).comp b

lemma

aR_eq_zero_of_mem

L89 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.aR_eq_zero_of_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section algebra
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]
  (ι₁ : A₁ →+* A) [IsLocalHom ι₁]
variable (hres₁ : Function.Surjective ((residue A).comp ι₁)) {R : Type u} [CommRing R] (b : A₁ →+*
  R)

Lean source · statement

lemma aR_eq_zero_of_mem {t : A} (ht : t ∈ maximalIdeal A) : aR ι₁ hres₁ b t = 0

lemma

ringHom_ext_of_ι₁

L93 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.ringHom_ext_of_ι₁

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section algebra
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]
  (ι₁ : A₁ →+* A) [IsLocalHom ι₁]
variable (hres₁ : Function.Surjective ((residue A).comp ι₁)) {R : Type u} [CommRing R] (b : A₁ →+*
  R)
include hres₁ in
omit [IsLocalRing A₁] [IsLocalHom ι₁] in

Lean source · statement

lemma ringHom_ext_of_ι₁ {T : Type*} [CommRing T] (φ ψ : A →+* T)
    (hφ : ∀ t ∈ maximalIdeal A, φ t = 0) (hψ : ∀ t ∈ maximalIdeal A, ψ t = 0)
    (h : ∀ a₁, φ (ι₁ a₁) = ψ (ι₁ a₁)) : φ = ψ

lemma

map_op_congr

L109 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.map_op_congr

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section thin
variable {Z : Scheme.{u}}

Lean source · statement

lemma map_op_congr {A B : Z.Opens} (i j : B ⟶ A) (s : Γ(Z, A)) :
    Z.presheaf.map i.op s = Z.presheaf.map j.op s

lemma

app_map_top

L112 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.app_map_top

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section thin
variable {Z : Scheme.{u}}

Lean source · statement

lemma app_map_top {Z' : Scheme.{u}} (q : Z' ⟶ Z) (W : Z.Opens) (x : Γ(Z, ⊤)) :
    q.app W (Z.presheaf.map (homOfLE le_top).op x) =
      Z'.presheaf.map (homOfLE le_top).op (q.appTop x)

lemma

comp_app_apply

L119 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.comp_app_apply

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section thin
variable {Z : Scheme.{u}}

Lean source · statement

lemma comp_app_apply {X Y : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) (x : Γ(Z, U)) :
    (f ≫ g).app U x = f.app (g ⁻¹ᵁ U) (g.app U x)

lemma

map_id_apply'

L121 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.map_id_apply'

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section thin
variable {Z : Scheme.{u}}

Lean source · statement

lemma map_id_apply' {A : Z.Opens} (i : A ⟶ A) (s : Γ(Z, A)) : Z.presheaf.map i.op s = s

lemma

map_congr'

L123 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.map_congr'

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section thin
variable {Z : Scheme.{u}}

Lean source · statement

lemma map_congr' {A B : Z.Opens} (i j : op A ⟶ op B) (s : Γ(Z, A)) :
    Z.presheaf.map i s = Z.presheaf.map j s

lemma

map_map_eq

L126 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.map_map_eq

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section thin
variable {Z : Scheme.{u}}

Lean source · statement

lemma map_map_eq {A B C : Z.Opens} (i : op A ⟶ op B) (j : op B ⟶ op C) (s : Γ(Z, A)) :
    Z.presheaf.map j (Z.presheaf.map i s) = Z.presheaf.map (i ≫ j) s

lemma

map_top_endo

L129 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.map_top_endo

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section thin
variable {Z : Scheme.{u}}

Lean source · statement

lemma map_top_endo (i : op (⊤ : Z.Opens) ⟶ op ⊤) (s : Γ(Z, ⊤)) : Z.presheaf.map i s = s

def

baseAt

L138 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.baseAt

Documentation

The base ring homomorphism into the stalk at a scheme point.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section scheme
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]

Lean source · statement

def baseAt {B : Type u} [CommRing B] {Y : Scheme.{u}} (f : Y ⟶ Spec (CommRingCat.of
  B))
    (y : Y) : B →+* Y.presheaf.stalk y

lemma

baseAt_apply

L144 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.baseAt_apply

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section scheme
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]

Lean source · statement

lemma baseAt_apply {B : Type u} [CommRing B] {Y : Scheme.{u}} (f : Y ⟶ Spec (CommRingCat.of B)) (y
  : Y)
    (t : B) : baseAt f y t = Y.presheaf.germ ⊤ y trivial (f.appTop ((Scheme.ΓSpecIso
      (CommRingCat.of B)).inv t))

lemma

fromSpecStalk_comp_baseAt

L150 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.fromSpecStalk_comp_baseAt

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section scheme
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]

Lean source · statement

lemma fromSpecStalk_comp_baseAt {B : Type u} [CommRing B] {Y : Scheme.{u}}
    (f : Y ⟶ Spec (CommRingCat.of B)) (y : Y) :
    Y.fromSpecStalk y ≫ f = Spec.map (CommRingCat.ofHom (baseAt f y))

lemma

baseAt_mem_maximalIdeal

L159 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.baseAt_mem_maximalIdeal

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section scheme
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]

Lean source · statement

lemma baseAt_mem_maximalIdeal {B : Type u} [CommRing B] [IsLocalRing B] {Y : Scheme.{u}}
    (f : Y ⟶ Spec (CommRingCat.of B)) (y : Y) (hy : f.base y = closedPoint B) {t : B} (ht : t ∈
      maximalIdeal B) :
    baseAt f y t ∈ maximalIdeal (Y.presheaf.stalk y)

lemma

stalkMap_baseAt

L172 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.stalkMap_baseAt

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section scheme
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]
omit [IsLocalRing A] [IsLocalRing A₁] in

Lean source · statement

lemma stalkMap_baseAt (ι₁ : A₁ →+* A) {X₁ P : Scheme.{u}} (f₁ : X₁ ⟶ Spec (CommRingCat.of A₁))
    (π : P ⟶ X₁) (β : P ⟶ Spec (CommRingCat.of A))
    (hw : π ≫ f₁ = β ≫ Spec.map (CommRingCat.ofHom ι₁)) (p : P) (a₁ : A₁) :
    (π.stalkMap p).hom (baseAt f₁ (π.base p) a₁) = baseAt β p (ι₁ a₁)

lemma

germ_stalkMap_stalkClosedPointTo

L186 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.germ_stalkMap_stalkClosedPointTo

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section scheme
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]

Lean source · statement

lemma germ_stalkMap_stalkClosedPointTo
    {R : CommRingCat.{u}} [IsLocalRing R] {X Y : Scheme.{u}}
    (σ : Spec R ⟶ X) (p : X) (hp : σ (closedPoint R) = p) (g : X ⟶ Y)
    (U : Y.Opens) (hU : g p ∈ U) (hU' : (σ ≫ g) (closedPoint R) ∈ U) :
    Y.presheaf.germ U (g p) hU ≫ g.stalkMap p ≫
        (X.presheaf.stalkCongr (Inseparable.of_eq hp)).inv ≫ Scheme.stalkClosedPointTo σ =
      Y.presheaf.germ U ((σ ≫ g) (closedPoint R)) hU' ≫
        Scheme.stalkClosedPointTo (σ ≫ g)

theorem

core

L199 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback.CFStalk.core

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
namespace CFStalk
section scheme
variable {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]

Lean source · statement

theorem core (ι₁ : A₁ →+* A) [IsLocalHom ι₁] (hres₁ : Function.Surjective ((residue A).comp ι₁))
    {X₁ P : Scheme.{u}} (f₁ : X₁ ⟶ Spec (CommRingCat.of A₁))
    (π : P ⟶ X₁) (β : P ⟶ Spec (CommRingCat.of A))
    (hP : IsPullback π β f₁ (Spec.map (CommRingCat.ofHom ι₁)))
    (p : P) (hp : β.base p = closedPoint A)
    (r : X₁.presheaf.stalk (π.base p))
    (hr : (π.stalkMap p).hom r ∈ Ideal.map (baseAt β p) (maximalIdeal A)) :
    r ∈ Ideal.map (baseAt f₁ (π.base p)) (maximalIdeal A₁)

theorem

mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback

L369 ↗

AlgebraicGeometry.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace IsLocalRing
open CFStalk in

Lean source · statement

theorem
  _root_.AlgebraicGeometry.mem_map_maximalIdeal_of_stalkMap_mem_map_maximalIdeal_of_iso_pullback
    {A A₁ : Type u} [CommRing A] [IsLocalRing A] [CommRing A₁] [IsLocalRing A₁]
    (ι₁ : A₁ →+* A) [IsLocalHom ι₁] (hres₁ : Function.Surjective ((IsLocalRing.residue A).comp ι₁))
    {X X₁ : Scheme.{u}} (toBase : X ⟶ Spec (CommRingCat.of A)) (f₁ : X₁ ⟶ Spec (CommRingCat.of A₁))
    (e₁ : X ≅ pullback f₁ (Spec.map (CommRingCat.ofHom ι₁)))
    (he₁ : e₁.hom ≫ pullback.snd f₁ (Spec.map (CommRingCat.ofHom ι₁)) = toBase)
    (x : X) (hx : toBase.base x = IsLocalRing.closedPoint A)
    (r : X₁.presheaf.stalk ((e₁.hom ≫ pullback.fst f₁ (Spec.map (CommRingCat.ofHom ι₁))).base x))
    (hr : ((e₁.hom ≫ pullback.fst f₁ (Spec.map (CommRingCat.ofHom ι₁))).stalkMap x).hom r ∈
      Ideal.map ((X.presheaf.germ ⊤ x trivial).hom.comp
        (toBase.appTop.hom.comp (Scheme.ΓSpecIso (CommRingCat.of A)).inv.hom))
        (IsLocalRing.maximalIdeal A)) :
    r ∈ Ideal.map ((X₁.presheaf.germ ⊤ ((e₁.hom ≫ pullback.fst f₁ (Spec.map (CommRingCat.ofHom
      ι₁))).base x)
        trivial).hom.comp (f₁.appTop.hom.comp (Scheme.ΓSpecIso (CommRingCat.of A₁)).inv.hom))
      (IsLocalRing.maximalIdeal A₁)

Module documentation

mem map maximal Ideal of stalk Map mem map maximal Ideal of iso pullback

Declarations