isClosedImmersion_equalizer_ι_left

English

For morphisms f, g: X ⇒ Y in the over-category with Y separated, the left leg of the equalizer is a closed immersion.

Русский

Для морфизмов f, g: X ⇒ Y над S, левая ножка равнозамкнута как замкнутое вложение.

LaTeX

$$IsClosedImmersion\left(\mathrm{equalizer.ι}\ f\ g\right).left$$

Lean4

@[stacks 01KM]
instance isClosedImmersion_equalizer_ι_left {S : Scheme} {X Y : Over S} [IsSeparated Y.hom] (f g : X ⟶ Y) :
    IsClosedImmersion (equalizer.ι f g).left :=
  by
  refine MorphismProperty.of_isPullback ((Limits.isPullback_equalizer_prod f g).map (Over.forget _)).flip ?_
  rw [← MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion _ (Over.prodLeftIsoPullback Y Y).hom]
  convert (inferInstanceAs (IsClosedImmersion (pullback.diagonal Y.hom)))
  ext1 <;> simp [← Over.comp_left]

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