iff_isFinite_and_mono — Mathlib

English

A morphism is a closed immersion if and only if it is finite and mono.

Русский

Морфизм есть замкнутое вложение тогда и только тогда, когда он конечен и моно.

LaTeX

$$$\mathrm{IsClosedImmersion}(f) \iff \mathrm{IsFinite}(f) \wedge \mathrm{Mono}(f).$$$

Lean4

theorem _root_.AlgebraicGeometry.IsClosedImmersion.iff_isFinite_and_mono : IsClosedImmersion f ↔ IsFinite f ∧ Mono f :=
  by
  wlog hY : IsAffine Y
  · change _ ↔ _ ∧ monomorphisms _ f
    rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := @IsClosedImmersion) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := monomorphisms _) Y.affineCover]
    simp_rw [this, forall_and, monomorphisms]
  rw [HasAffineProperty.iff_of_isAffine (P := @IsClosedImmersion), HasAffineProperty.iff_of_isAffine (P := @IsFinite),
    RingHom.surjective_iff_epi_and_finite, @and_comm (Epi _), ← and_assoc]
  refine and_congr_right fun ⟨_, _⟩ ↦ Iff.trans ?_ (arrow_mk_iso_iff (monomorphisms _) (arrowIsoSpecΓOfIsAffine f).symm)
  trans Mono (f.app ⊤).op
  · exact ⟨fun h ↦ inferInstance, fun h ↦ show Epi (f.app ⊤).op.unop by infer_instance⟩
  exact (Functor.mono_map_iff_mono Scheme.Spec _).symm

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