Theorems · Theorem · algebraic geometry

AlgebraicGeometry.isIso_of_comp_eq_sigmaSpec

∀ {ι : Type u} (R : ι → CommRingCat) {V : AlgebraicGeometry.Scheme} (f : (∐ fun i => AlgebraicGeometry.Spec (R i)) ⟶ V)
  (g : V ⟶ AlgebraicGeometry.Spec (CommRingCat.of ((i : ι) → ↑(R i)))) [AlgebraicGeometry.IsImmersion g]
  [CompactSpace ↥V], CategoryTheory.CategoryStruct.comp f g = AlgebraicGeometry.sigmaSpec R → CategoryTheory.IsIso g

If V is a locally closed subscheme of Spec (Π Rᵢ) containing ∐ Spec Rᵢ, then V = Spec (Π Rᵢ).

Defined in

Mathlib.AlgebraicGeometry.PointsPi

Cited by

1 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsImmersionCompactSpace