Theorems · Theorem · commutative algebra

PrimeSpectrum.rankAtStalk_pos_iff_mem_range_comap

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Flat R S]
  [Module.Finite R S] (p : PrimeSpectrum R),
  0 < Module.rankAtStalk S p ↔ p ∈ Set.range (PrimeSpectrum.comap (algebraMap R S))

Defined in: Mathlib.RingTheory.Flat.Rank
Cited by: 2 results in Mathlib
Foundations: Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing Algebra Module.Flat Module.Finite

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites13

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

Setstatement · cited by 53,352
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
Algebra.algebraMapstatement and proof · cited by 4,706
Set.rangestatement and proof · cited by 4,705
Module.Finitestatement and proof · cited by 1,032
PrimeSpectrumstatement and proof · cited by 625
Module.Flatstatement and proof · cited by 279
PrimeSpectrum.comapstatement and proof · cited by 199
Module.rankAtStalkstatement · cited by 41
Module.finrank_pos_iffproof · cited by 8
Module.rankAtStalk_eqproof · cited by 2

Cited by2

Results whose statement or proof uses this declaration.

AlgebraicGeometry.Scheme.Hom.one_le_finrank_mapproof · cited by 1
AlgebraicGeometry.Scheme.Hom.one_le_finrank_iff_surjectiveproof · cited by 0