map_eq_top_or_isMaximal_of_surjective

English

For a surjective f and a family K:ι → Ideal S, map f of the infimum over i of (K(i).comap f) equals the infimum over i of K(i).

Русский

Пусть f сюръективно. Тогда map f от iInf (K(i).comap f) равен iInf (K(i)).

LaTeX

$$$hf : \mathrm{Function.Surjective}(f) \rightarrow \forall K : ι \to \mathrm{Ideal}(S), \; \mathrm{map}(f)(\bigwedge_i (K(i).comap f)) = \bigwedge_i K(i)$$$

Lean4

theorem map_eq_top_or_isMaximal_of_surjective (hf : Function.Surjective f) {I : Ideal R} (H : IsMaximal I) :
    map f I = ⊤ ∨ IsMaximal (map f I) :=
  or_iff_not_imp_left.2 fun ne_top ↦
    ⟨⟨ne_top, fun _J hJ ↦
        comap_injective_of_surjective f hf <|
          H.1.2 _ (le_comap_map.trans_lt <| (orderEmbeddingOfSurjective f hf).strictMono hJ)⟩⟩

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