comap_isInducing_of_surjective — Mathlib

English

If I ≤ nilradical(R), then the comap map associated to the quotient by I is bijective on prime spectra.

Русский

Если I ≤ нильрадикал(R), то отображение comap, соответствующее факторизации по I, биективно на спектрах.

LaTeX

$$For I, if hle : I ≤ nilradical(R), then Function.Bijective (comap <| Ideal.Quotient.mk I).$$

Lean4

theorem comap_isInducing_of_surjective (hf : Surjective f) : IsInducing (comap f) where
  eq_induced :=
    by
    simp only [TopologicalSpace.ext_iff, ← isClosed_compl_iff, isClosed_iff_zeroLocus, isClosed_induced_iff]
    refine fun s =>
      ⟨fun ⟨F, hF⟩ =>
        ⟨zeroLocus (f ⁻¹' F), ⟨f ⁻¹' F, rfl⟩, by
          rw [preimage_comap_zeroLocus, Function.Surjective.image_preimage hf, hF]⟩,
        ?_⟩
    rintro ⟨-, ⟨F, rfl⟩, hF⟩
    exact ⟨f '' F, hF.symm.trans (preimage_comap_zeroLocus f F)⟩

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