eq_bot_of_comp_quotientMk_eq_sigmaSpec

English

If a map f factors through Spec of a quotient by I so that the composition with the quotient map equals the universal sigmaSpec, then I is the zero ideal.

Русский

Если отображение f через спектр фактор-момета по I даёт композицию равную sigmaSpec, то I=0.

LaTeX

$$If f: ∐ Spec(R_i) → Spec(Π R_i / I) satisfies f ≫ Spec.map (Ideal.Quotient.mk I) = sigmaSpec R, then I = ⊥.$$

Lean4

theorem eq_bot_of_comp_quotientMk_eq_sigmaSpec (I : Ideal (Π i, R i))
    (f : (∐ fun i ↦ Spec (R i)) ⟶ Spec (.of <| (Π i, R i) ⧸ I))
    (hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R) : I = ⊥ :=
  by
  refine le_bot_iff.mp fun x hx ↦ ?_
  ext i
  simpa [← Category.assoc, Ideal.Quotient.eq_zero_iff_mem.mpr hx] using
    congr((Spec.preimage (Sigma.ι (Spec <| R ·) i ≫ $hf)).hom x).symm

Похожие утверждения