Residue fields of a base change with trivial residue field extension

Let R → R' be a ring map and P a prime of R' over a prime p of R with κ(p) = κ(P). Mathlib's Ideal.fiberIsoOfBijectiveResidueField identifies the primes of R' ⊗[R] S over P with the primes of S over p. This file adds that the identification does not change residue fields: for a prime Q of R' ⊗[R] S over P, the map κ(Q ∩ S) → κ(Q) is bijective (Ideal.ResidueField.bijective_map_includeRight).

This is how an étale neighbourhood (R', P) of p with trivial residue field extension, as produced by Mathlib's Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq (Stacks 00UJ), also preserves the residue field at the point of S it isolates.

For an ideal I contained in a prime P of an A-algebra W, the diagonal point of (W ⧸ I) ⊗[A] W over P, sending s ⊗ w to s(P) w(P) in κ(P), is the W-algebra map of Ideal.ResidueField.exists_algHom_tensorProduct_eq_lmul'.

theorem Ideal.ResidueField.bijective_map_includeRight {R : Type u_1} {R' : Type u_2} {S : Type u_3} [CommRing R] [CommRing R'] [CommRing S] [Algebra R R'] [Algebra R S] (p : Ideal R) [p.IsPrime] (P : Ideal R') [P.IsPrime] [P.LiesOver p] (q : Ideal S) [q.IsPrime] (Q : Ideal (TensorProduct R R' S)) [Q.IsPrime] [Q.LiesOver P] (hQ : q = comap Algebra.TensorProduct.includeRight.toRingHom Q) (H : Function.Bijective ⇑(mapₐ p P (Algebra.ofId R R') ⋯)) : Function.Bijective ⇑(map q Q Algebra.TensorProduct.includeRight.toRingHom hQ)

If P is a prime of R' over p with κ(p) = κ(P), and Q is a prime of R' ⊗[R] S over P with contraction q to S, then κ(q) → κ(Q) is bijective.

theorem Ideal.ResidueField.exists_algHom_tensorProduct_eq_lmul' (A : Type u_4) {W : Type u_5} [CommRing A] [CommRing W] [Algebra A W] (I P : Ideal W) [P.IsPrime] (hIP : I ≤ P) : ∃ (ψ : TensorProduct A (W ⧸ I) W →ₐ[W] P.ResidueField), ∀ (z : TensorProduct A (W ⧸ I) W), ψ z = (Quotient.liftₐ I (IsScalarTower.toAlgHom A W P.ResidueField) ⋯) ((Algebra.TensorProduct.lmul' A) ((Algebra.TensorProduct.map (AlgHom.id A (W ⧸ I)) (Quotient.mkₐ A I)) z))

The diagonal point of (W ⧸ I) ⊗[A] W over a prime P ⊇ I: the W-algebra map to κ(P) sending s ⊗ w to s(P) w(P). It factors through multiplication on (W ⧸ I) ⊗[A] (W ⧸ I).