isOpenImmersion_SpecMap_iff_of_surjective

English

Spec.map for a surjective ring hom is an open immersion iff ker is generated by an idempotent.

Русский

Spec.map для сюръективного кольцевого гомоморфизма есть открытое вложение тогда и только тогда, когда ядро порождено идемпотентом.

LaTeX

$$$ IsOpenImmersion(\mathrm{Spec.map} f) \iff \exists e\ IsIdempotentElem(e) \land \ker f.hom = \langle e \rangle $$$

Lean4

/-- `Spec (R ⧸ I) ⟶ Spec R` is an open immersion iff `I` is generated by an idempotent. -/
theorem isOpenImmersion_SpecMap_iff_of_surjective {R S : CommRingCat} (f : R ⟶ S) (hf : Function.Surjective f.hom) :
    IsOpenImmersion (Spec.map f) ↔ ∃ e, IsIdempotentElem e ∧ RingHom.ker f.hom = Ideal.span { e } :=
  by
  constructor
  · intro H
    obtain ⟨e, he, he'⟩ :=
      PrimeSpectrum.isClopen_iff_zeroLocus.mp
        ⟨PrimeSpectrum.isClosed_range_comap_of_surjective _ _ hf, (Spec.map f).isOpenEmbedding.isOpen_range⟩
    refine ⟨e, he, ?_⟩
    let φ : R ⟶ _ := (CommRingCat.ofHom (Ideal.Quotient.mk (.span { e })))
    have : IsOpenImmersion (Spec.map φ) :=
      have : IsLocalization.Away (1 - e) (↑R ⧸ Ideal.span { e }) :=
        IsLocalization.away_of_isIdempotentElem he.one_sub (by simp) Ideal.Quotient.mk_surjective
      IsOpenImmersion.of_isLocalization (1 - e)
    have H : Set.range (Spec.map φ).base = Set.range (Spec.map f).base :=
      ((PrimeSpectrum.range_comap_of_surjective _ _ Ideal.Quotient.mk_surjective).trans (by simp)).trans he'.symm
    let i : S ≅ .of _ := (Scheme.Spec.preimageIso (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
    have hi : Function.Injective i.inv.hom := (ConcreteCategory.bijective_of_isIso i.inv).1
    have : f = φ ≫ i.inv := by apply Spec.map_injective; simp [i, ← Scheme.Spec_map]
    rw [this, CommRingCat.hom_comp, RingHom.ker_eq_comap_bot, ← Ideal.comap_comap, ← RingHom.ker_eq_comap_bot,
      (RingHom.injective_iff_ker_eq_bot i.inv.hom).mp hi, ← RingHom.ker_eq_comap_bot]
    simp [φ]
  · rintro ⟨e, he, he'⟩
    letI := f.hom.toAlgebra
    have : IsLocalization.Away (1 - e) S := IsLocalization.away_of_isIdempotentElem he.one_sub (by simpa using he') hf
    exact IsOpenImmersion.of_isLocalization (1 - e)

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