isCompact_image_comap_of_monic — Mathlib

English

If f and g ∈ R[X] with g monic, then the image of comap along C of Z(g) \\ Z(f) is a compact subset of Spec(R).

Русский

Если f и g ∈ R[X] с g моническим, то образ comap C '' (Z(g) \\ Z(f)) является компактной подмножеством Spec(R).

LaTeX

$$IsCompact( comap C '' (Z(g) \\ Z(f)) )$$

Lean4

theorem isCompact_image_comap_of_monic (f g : R[X]) (hg : g.Monic) :
    IsCompact (comap C '' (zeroLocus { g } \ zeroLocus { f })) :=
  by
  obtain ⟨t, ht⟩ := exists_image_comap_of_monic f g hg
  rw [ht, ← t.toSet.iUnion_of_singleton_coe, zeroLocus_iUnion, Set.compl_iInter]
  apply isCompact_iUnion
  exact fun _ ↦ by simpa using isCompact_basicOpen _

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