Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_f

∀ {R : CommRingCat} {ι : Type u_1} (s : ι → ↑R) (hs : Ideal.span (Set.range s) = ⊤) (i : ι),
  (AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop s hs).f i =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (s i))))

Defined in: Mathlib.AlgebraicGeometry.Cover.Open
Cited by: 1 results in Mathlib
Foundations: Depth 133 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites17

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

Quiver.Homstatement · cited by 32,603
Top.topstatement and proof · cited by 9,680
Idealstatement · cited by 4,748
Algebra.algebraMapstatement · cited by 4,706
Set.rangestatement and proof · cited by 4,705
AlgebraicGeometry.Schemestatement · cited by 2,540
CommRingCatstatement and proof · cited by 2,333
CommRingCat.carrierstatement and proof · cited by 1,096
Ideal.spanstatement and proof · cited by 948
AlgebraicGeometry.Specstatement · cited by 626
AlgebraicGeometry.IsOpenImmersionstatement · cited by 476
Submonoid.powersstatement · cited by 408

Cited by1

Results whose statement or proof uses this declaration.

AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty_of_isZariskiLocalAtSource_of_isZariskiLocalAtTargetproof · cited by 1