English
If V with an immersion into Spec of a product contains the affine sum and the maps factor with the sigmaSpec condition, then the immersion g is an isomorphism.
Русский
Если V с внедрением в Spec произведения содержит образ себи и морфизмы удовлетворяют условиям sigmaSpec, то вложение g является изоморфизмом.
LaTeX
$$IsIso g under [IsImmersion g], [CompactSpace V], with f: (∐ Spec R_i) ⟶ V, and f ≫ g = sigmaSpec R, then g is an isomorphism.$$
Lean4
/-- If `V` is a locally closed subscheme of `Spec (Π Rᵢ)` containing `∐ Spec Rᵢ`, then
`V = Spec (Π Rᵢ)`. -/
theorem isIso_of_comp_eq_sigmaSpec {V : Scheme} (f : (∐ fun i ↦ Spec (R i)) ⟶ V) (g : V ⟶ Spec (.of <| Π i, R i))
[IsImmersion g] [CompactSpace V] (hU' : f ≫ g = sigmaSpec R) : IsIso g :=
by
have : g.coborderRange = ⊤ :=
by
apply eq_top_of_sigmaSpec_subset_of_isCompact (hVU := subset_coborder)
· simpa only [← hU'] using Set.range_comp_subset_range f.base g.base
· exact isCompact_range g.base.hom.2
have : IsClosedImmersion g :=
by
have : IsIso g.coborderRange.ι := by rw [this, ← Scheme.topIso_hom]; infer_instance
rw [← g.liftCoborder_ι]
infer_instance
obtain ⟨I, e, rfl⟩ := IsClosedImmersion.Spec_iff.mp this
obtain rfl := eq_bot_of_comp_quotientMk_eq_sigmaSpec R I (f ≫ e.hom) (by rwa [Category.assoc])
convert_to IsIso (e.hom ≫ Spec.map (RingEquiv.quotientBot _).toCommRingCatIso.inv)
infer_instance
