Theorems · Theorem · algebraic geometry

PrimeSpectrum.preimageEquivFiber_apply_asIdeal

∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : PrimeSpectrum R)
  (q : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p})),
  ((PrimeSpectrum.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

Defined in: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Cited by: 2 results in Mathlib
Foundations: Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites25

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement · cited by 53,352
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
RingHomstatement · cited by 10,189
Equivstatement · cited by 8,337
Set.Elemstatement and proof · cited by 7,166
Set.preimagestatement and proof · cited by 4,946
Idealstatement · cited by 4,748
Algebra.algebraMapstatement and proof · cited by 4,706
TensorProductstatement · cited by 2,545
PrimeSpectrumstatement and proof · cited by 625

Cited by2

Results whose statement or proof uses this declaration.

Ideal.exists_not_mem_forall_mem_of_ne_of_liesOverproof · cited by 1
Localization.exists_finite_awayMapₐ_of_surjective_awayMapₐproof · cited by 1