le_map_iff_comap_le — Mathlib

English

For ideals J on Y and morphism f: X → Y, J ≤ I.map f iff J.comap f ≤ I.

Русский

Для идеалов J на Y и морфизма f: X → Y верно: J ≤ I.map f тогда и только тогда, J.comap f ≤ I.

LaTeX

$$$J \le I.map f \;\iff\; J. comap f \le I$$$

Lean4

theorem le_map_iff_comap_le {I : X.IdealSheafData} {f : X ⟶ Y} {J : Y.IdealSheafData} : J ≤ I.map f ↔ J.comap f ≤ I :=
  by
  constructor
  · intro H
    rw [← I.ker_subschemeι, ←
      pullback.lift_fst (f := f) (g := J.subschemeι) I.subschemeι ((I.subschemeι ≫ f).toImage ≫ inclusion H) (by simp)]
    exact Hom.le_ker_comp _ _
  · intro H
    have : (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd _ _) ≫ J.subschemeι = I.subschemeι ≫ f := by
      simp [← pullback.condition]
    rw [map, ← J.ker_subschemeι, ← this]
    exact Hom.le_ker_comp _ _

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