Field-valued points and residue-field data

An algebra map to a field determines a prime ideal and an embedding of its residue field. Conversely, these data determine the algebra map. For a map to the residue field κ(P) of a prime P of the base, the embedding is an isomorphism (AlgHom.residueFieldMap_bijective). The forward map from residue-field data is defined for any commutative target algebra.

References

• Stacks Project, Tag 04GW.
• Taylor Dupuy, Thomas Tucker, and Zhuoran Wang, pcfawd-formalization at 9a20b3f, lean/Pcf/Stacks/Abhyankar/StrictHenselizationConstruction.lean, PointedEtaleNeighborhood.

theorem AlgHom.instIsPrimeKer_tauCeti {R : Type u_1} {S : Type u_2} {Ω : Type u_3} [CommRing R] [CommRing S] [Field Ω] [Algebra R S] [Algebra R Ω] (point : S →ₐ[R] Ω) : (RingHom.ker point).IsPrime

noncomputable def AlgHom.residueEmbedding {R : Type u_1} {S : Type u_2} {Ω : Type u_3} [CommRing R] [CommRing S] [Field Ω] [Algebra R S] [Algebra R Ω] (point : S →ₐ[R] Ω) : (RingHom.ker point).ResidueField →ₐ[R] Ω

The residue-field embedding induced by a field-valued point.

@[simp]

theorem AlgHom.residueEmbedding_comp {R : Type u_1} {S : Type u_2} {Ω : Type u_3} [CommRing R] [CommRing S] [Field Ω] [Algebra R S] [Algebra R Ω] (point : S →ₐ[R] Ω) : point.residueEmbedding.comp (IsScalarTower.toAlgHom R S (RingHom.ker point).ResidueField) = point

The residue-field embedding recovers the original point.

theorem AlgHom.existsUnique_residueEmbedding {R : Type u_1} {S : Type u_2} {Ω : Type u_3} [CommRing R] [CommRing S] [Field Ω] [Algebra R S] [Algebra R Ω] (point : S →ₐ[R] Ω) : ∃! embedding : (RingHom.ker point).ResidueField →ₐ[R] Ω, embedding.comp (IsScalarTower.toAlgHom R S (RingHom.ker point).ResidueField) = point

A field-valued point factors uniquely through the residue field of its kernel.

theorem AlgHom.comap_ker_eq_of_residueField {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : Ideal R} [P.IsPrime] (point : S →ₐ[R] P.ResidueField) : Ideal.comap (algebraMap R S) (RingHom.ker point) = P

The kernel of an R-algebra map to the residue field κ(P) of a prime P of R lies over P.

theorem AlgHom.residueFieldMap_bijective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : Ideal R} [P.IsPrime] (point : S →ₐ[R] P.ResidueField) : Function.Bijective ⇑(Ideal.ResidueField.map P (RingHom.ker point) (algebraMap R S) ⋯)

An R-algebra map from S to the residue field κ(P) of a prime P of R identifies κ(P) with the residue field of S at its kernel.

theorem Ideal.exists_algebra_residueField_isScalarTower {R : Type u_1} {F : Type u_2} [CommRing R] [Field F] [Algebra R F] (p : Ideal R) [p.IsPrime] (hp : RingHom.ker (algebraMap R F) = p) : ∃ (x : Algebra p.ResidueField F), IsScalarTower R p.ResidueField F

If a prime p of R is the kernel of a map R → F to a field, then F is an algebra over the residue field κ(p), compatibly with the algebra structures over R. For p = RingHom.ker (algebraMap R F) the map κ(p) → F is AlgHom.residueEmbedding.

@[simp]

theorem Ideal.ker_residueEmbedding_comp {R : Type u_1} {S : Type u_2} {Ω : Type u_3} [CommRing R] [CommRing S] [CommRing Ω] [Algebra R S] [Algebra R Ω] (prime : Ideal S) [prime.IsPrime] [Nontrivial Ω] (embedding : prime.ResidueField →ₐ[R] Ω) : RingHom.ker (embedding.comp (IsScalarTower.toAlgHom R S prime.ResidueField)) = prime

A residue-field embedding recovers the prime through its kernel.

theorem Ideal.residueEmbedding_comp_map_iff {R : Type u_1} {S : Type u_2} {Ω : Type u_3} [CommRing R] [CommRing S] [CommRing Ω] [Algebra R S] [Algebra R Ω] {T : Type u_4} [CommRing T] [Algebra R T] (sourcePrime : Ideal S) [sourcePrime.IsPrime] (targetPrime : Ideal T) [targetPrime.IsPrime] (sourceEmbedding : sourcePrime.ResidueField →ₐ[R] Ω) (targetEmbedding : targetPrime.ResidueField →ₐ[R] Ω) (morphism : S →ₐ[R] T) (hprime : sourcePrime = comap morphism.toRingHom targetPrime) : targetEmbedding.comp (ResidueField.mapₐ sourcePrime targetPrime morphism hprime) = sourceEmbedding ↔ (targetEmbedding.comp (IsScalarTower.toAlgHom R T targetPrime.ResidueField)).comp morphism = sourceEmbedding.comp (IsScalarTower.toAlgHom R S sourcePrime.ResidueField)

Compatibility of residue embeddings is exactly compatibility of the associated points.

@[reducible, inline]

abbrev TauCeti.ResidueField.PointData (R : Type u_4) (S : Type u_5) (Ω : Type u_6) [CommRing R] [CommRing S] [CommRing Ω] [Algebra R S] [Algebra R Ω] : Type (max u_5 u_6 u_5)

A prime and an algebra map from its residue field to the chosen algebra.

noncomputable def TauCeti.ResidueField.PointData.toAlgHom {R : Type u_1} {S : Type u_2} {Ω : Type u_3} [CommRing R] [CommRing S] [CommRing Ω] [Algebra R S] [Algebra R Ω] (data : PointData R S Ω) : S →ₐ[R] Ω

The algebra-valued point associated with residue-field data.

@[simp]

theorem TauCeti.ResidueField.PointData.toAlgHom_apply {R : Type u_1} {S : Type u_2} {Ω : Type u_3} [CommRing R] [CommRing S] [CommRing Ω] [Algebra R S] [Algebra R Ω] (data : PointData R S Ω) (element : S) : data.toAlgHom element = data.snd ((algebraMap S data.fst.asIdeal.ResidueField) element)

Evaluate the point induced by residue-field data.

theorem TauCeti.ResidueField.PointData.toAlgHom_injective {R : Type u_1} {S : Type u_2} {Ω : Type u_3} [CommRing R] [CommRing S] [CommRing Ω] [Nontrivial Ω] [Algebra R S] [Algebra R Ω] : Function.Injective toAlgHom

Residue-field data are determined by their algebra-valued point.

theorem TauCeti.ResidueField.instIsPrimeKerAlgHom_tauCeti {R : Type u_1} {S : Type u_2} {Ω : Type u_3} [CommRing R] [CommRing S] [Field Ω] [Algebra R S] [Algebra R Ω] (point : S →ₐ[R] Ω) : (RingHom.ker point).IsPrime

theorem TauCeti.ResidueField.PointData.toAlgHom_bijective {R : Type u_1} {S : Type u_2} {Ω : Type u_3} [CommRing R] [CommRing S] [Field Ω] [Algebra R S] [Algebra R Ω] : Function.Bijective toAlgHom

Residue-field data determine the point bijectively.

noncomputable def TauCeti.ResidueField.pointDataEquiv {R : Type u_1} {S : Type u_2} {Ω : Type u_3} [CommRing R] [CommRing S] [Field Ω] [Algebra R S] [Algebra R Ω] : PointData R S Ω ≃ (S →ₐ[R] Ω)

Field-valued points are equivalent to a prime and a residue-field embedding.

@[simp]

theorem TauCeti.ResidueField.pointDataEquiv_apply {R : Type u_1} {S : Type u_2} {Ω : Type u_3} [CommRing R] [CommRing S] [Field Ω] [Algebra R S] [Algebra R Ω] (data : PointData R S Ω) : pointDataEquiv data = data.toAlgHom

The forward correspondence is the point induced by the residue-field embedding.

@[simp]

theorem TauCeti.ResidueField.pointDataEquiv_symm_apply {R : Type u_1} {S : Type u_2} {Ω : Type u_3} [CommRing R] [CommRing S] [Field Ω] [Algebra R S] [Algebra R Ω] (point : S →ₐ[R] Ω) : pointDataEquiv.symm point = ⟨{ asIdeal := RingHom.ker point, isPrime := ⋯ }, point.residueEmbedding⟩

The inverse correspondence assigns a point its kernel and residue-field embedding.

theorem TauCeti.ResidueField.PointData.toAlgHom_comp_iff {R : Type u_1} {S : Type u_2} {Ω : Type u_3} [CommRing R] [CommRing S] [CommRing Ω] [Nontrivial Ω] [Algebra R S] [Algebra R Ω] {T : Type u_4} [CommRing T] [Algebra R T] (source : PointData R S Ω) (target : PointData R T Ω) (morphism : S →ₐ[R] T) : target.toAlgHom.comp morphism = source.toAlgHom ↔ ∃ (hprime : source.fst.asIdeal = Ideal.comap morphism.toRingHom target.fst.asIdeal), target.snd.comp (Ideal.ResidueField.mapₐ source.fst.asIdeal target.fst.asIdeal morphism hprime) = source.snd

Compatibility of induced points is compatibility of the prime and residue-field maps.