The fiber of a ring homomorphism at a prime ideal

Main results

• Ideal.Fiber: p.Fiber S is the fiber of a prime p of R in an R-algebra S, defined to be κ(p) ⊗ S.
• PrimeSpectrum.preimageHomeomorphFiber : We show that there is a homeomorphism between the fiber of the induced map PrimeSpectrum S → PrimeSpectrum R at a prime ideal p and the prime spectrum of p.Fiber S.

instance instIsLocalRingTensorProductResidueFieldOfIsLocalHomRingHomAlgebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] : IsLocalRing (TensorProduct R (IsLocalRing.ResidueField R) S)

theorem Ideal.ResidueField.exists_smul_eq_tmul_one {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (x : TensorProduct R S p.ResidueField) : ∃ r ∉ p, ∃ (s : S), r • x = s ⊗ₜ[R] 1

@[reducible, inline]

abbrev Ideal.Fiber {R : Type u_1} [CommRing R] (p : Ideal R) [p.IsPrime] (S : Type u_3) [AddCommGroup S] [Module R S] : Type (max u_3 u_1)

The fiber of a prime p of R in an R-algebra S, defined to be κ(p) ⊗ S.

See PrimeSpectrum.preimageHomeomorphFiber for the homeomorphism between the spectrum of it and the actual set-theoretic fiber of PrimeSpectrum S → PrimeSpectrum R at p.

Equations

• p.Fiber S = TensorProduct R p.ResidueField S

instance instLiesOverFiberOfIsPrime {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (q : Ideal (p.Fiber S)) [q.IsPrime] : q.LiesOver p

theorem Ideal.Fiber.exists_smul_eq_one_tmul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (x : p.Fiber S) : ∃ r ∉ p, ∃ (s : S), r • x = 1 ⊗ₜ[R] s

noncomputable def Fiber.algEquivQuotient {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] : p.Fiber S ≃ₐ[S] Localization (Algebra.algebraMapSubmonoid S p.primeCompl) ⧸ Ideal.map (algebraMap (Localization p.primeCompl) (Localization (Algebra.algebraMapSubmonoid S p.primeCompl))) (IsLocalRing.maximalIdeal (Localization p.primeCompl))

p.Fiber S is isomorphic to the quotient Sₚ ⧸ pSₚ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PrimeSpectrum.preimageEquivFiber (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R) : ↑(comap (algebraMap R S) ⁻¹' {p}) ≃ PrimeSpectrum (p.asIdeal.Fiber S)

The fiber PrimeSpectrum S → PrimeSpectrum R at a prime ideal p : PrimeSpectrum R is in bijection with the prime spectrum of κ(p) ⊗[R] S.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PrimeSpectrum.preimageEquivFiber_apply_asIdeal (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R) (q : ↑(comap (algebraMap R S) ⁻¹' {p})) : ((preimageEquivFiber R S p) q).asIdeal = RingHom.ker (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (Algebra.ofId R S) ⋯) (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom

@[simp]

theorem PrimeSpectrum.preimageEquivFiber_symm_apply_coe (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R) (q : PrimeSpectrum (p.asIdeal.Fiber S)) : ↑((preimageEquivFiber R S p).symm q) = comap Algebra.TensorProduct.includeRight.toRingHom q

noncomputable def PrimeSpectrum.preimageOrderIsoFiber (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R) : ↑(comap (algebraMap R S) ⁻¹' {p}) ≃o PrimeSpectrum (p.asIdeal.Fiber S)

The OrderIso between the fiber of PrimeSpectrum S → PrimeSpectrum R at a prime ideal p : PrimeSpectrum R and the prime spectrum of κ(p) ⊗[R] S.

Equations

• PrimeSpectrum.preimageOrderIsoFiber R S p = { toEquiv := PrimeSpectrum.preimageEquivFiber R S p, map_rel_iff' := ⋯ }

@[simp]

theorem PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R) (q : PrimeSpectrum (p.asIdeal.Fiber S)) : ↑(↑((RelIso.symm (preimageOrderIsoFiber R S p)) q)).asIdeal = ⇑Algebra.TensorProduct.includeRight ⁻¹' ↑q.asIdeal

@[simp]

theorem PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R) (q : ↑(comap (algebraMap R S) ⁻¹' {p})) : ↑((preimageOrderIsoFiber R S p) q).asIdeal = ⇑(Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (Algebra.ofId R S) ⋯) (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯) ⁻¹' {0}

@[deprecated PrimeSpectrum.preimageOrderIsoFiber (since := "2025-12-07")]

def PrimeSpectrum.preimageOrderIsoTensorResidueField (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R) : ↑(comap (algebraMap R S) ⁻¹' {p}) ≃o PrimeSpectrum (p.asIdeal.Fiber S)

Alias of PrimeSpectrum.preimageOrderIsoFiber.

---

The OrderIso between the fiber of PrimeSpectrum S → PrimeSpectrum R at a prime ideal p : PrimeSpectrum R and the prime spectrum of κ(p) ⊗[R] S.

Equations

• PrimeSpectrum.preimageOrderIsoTensorResidueField = PrimeSpectrum.preimageOrderIsoFiber

noncomputable def PrimeSpectrum.primesOverOrderIsoFiber (R : Type u_3) (S : Type u_4) [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S)

The OrderIso between the set of primes lying over a prime ideal p : Ideal R, and the prime spectrum of κ(p) ⊗[R] S.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal (R : Type u_3) (S : Type u_4) [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (a✝ : ↑(p.primesOver S)) : ↑((primesOverOrderIsoFiber R S p) a✝).asIdeal = ⇑(Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p (↑a✝) (Algebra.ofId R S) ⋯) (IsScalarTower.toAlgHom R S (↑a✝).ResidueField) ⋯) ⁻¹' {0}

@[simp]

theorem PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe (R : Type u_3) (S : Type u_4) [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (a✝ : PrimeSpectrum (p.Fiber S)) : ↑↑((RelIso.symm (primesOverOrderIsoFiber R S p)) a✝) = ⇑Algebra.TensorProduct.includeRight ⁻¹' ↑a✝.asIdeal

noncomputable def PrimeSpectrum.preimageHomeomorphFiber (R : Type u_3) (S : Type u_4) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R) : ↑(comap (algebraMap R S) ⁻¹' {p}) ≃ₜ PrimeSpectrum (p.asIdeal.Fiber S)

The Homeomorph between the fiber of PrimeSpectrum S → PrimeSpectrum R at a prime ideal p : PrimeSpectrum R and the prime spectrum of κ(p) ⊗[R] S.

Equations

• PrimeSpectrum.preimageHomeomorphFiber R S p = { toEquiv := (PrimeSpectrum.preimageOrderIsoFiber R S p).toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal (R : Type u_3) (S : Type u_4) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R) (q : ↑(comap (algebraMap R S) ⁻¹' {p})) : ↑((preimageHomeomorphFiber R S p) q).asIdeal = ⇑(Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (Algebra.ofId R S) ⋯) (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯) ⁻¹' {0}

@[simp]

theorem PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal (R : Type u_3) (S : Type u_4) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R) (q : PrimeSpectrum (p.asIdeal.Fiber S)) : ↑(↑((preimageHomeomorphFiber R S p).symm q)).asIdeal = ⇑Algebra.TensorProduct.includeRight ⁻¹' ↑q.asIdeal