support_comap — Mathlib

English

The comap of a kernel under a composition equals the successive comaps, i.e., comap f then comap g equals comap (f ≫ g).

Русский

Comap ядра при композиции равен последовательным comap: comap f затем comap g равно comap (f ≫ g).

LaTeX

$$$I.c\,\mathrm{omap}(f ≫ g) = (I.c\,\mathrm{omap} g).comap f$$$

Lean4

@[simp]
theorem support_comap (I : Y.IdealSheafData) (f : X ⟶ Y) : (I.comap f).support = I.support.preimage f.continuous :=
  by
  ext1
  rw [comap, Scheme.Hom.support_ker, Pullback.range_fst, range_subschemeι, TopologicalSpace.Closeds.coe_preimage,
    (I.support.isClosed.preimage f.continuous).closure_eq]

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