Theorems · Theorem · algebraic geometry

AlgebraicGeometry.eq_bot_of_comp_quotientMk_eq_sigmaSpec

∀ {ι : Type u} (R : ι → CommRingCat) (I : Ideal ((i : ι) → ↑(R i)))
  (f : (∐ fun i => AlgebraicGeometry.Spec (R i)) ⟶ AlgebraicGeometry.Spec (CommRingCat.of (((i : ι) → ↑(R i)) ⧸ I))),
  CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) =
      AlgebraicGeometry.sigmaSpec R →
    I = ⊥

Defined in

Mathlib.AlgebraicGeometry.PointsPi

Cited by

1 results in Mathlib

Foundations

Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound