comap_prime — Mathlib

English

Let f: M → N and g: N → M be homomorphisms with g ∘ f = id_M. If f(p) is prime in N, then p is prime in M.

Русский

Пусть f: M → N и g: N → M — гомоморфизмы с выполненным g∘f = id_M. Если f(p) простое в N, то p простое в M.

LaTeX

$$(g ∘ f = id_M) ⇒ ∀ p : M, \\operatorname{Prime}(f(p)) ⇒ \\operatorname{Prime}(p).$$

Lean4

theorem comap_prime (hinv : ∀ a, g (f a : N) = a) (hp : Prime (f p)) : Prime p :=
  ⟨fun h => hp.1 <| by simp [h], fun h => hp.2.1 <| h.map f, fun a b h => by
    refine
        (hp.2.2 (f a) (f b) <| by
              convert map_dvd f h
              simp).imp
          ?_ ?_ <;>
      · intro h
        convert ← map_dvd g h <;> apply hinv⟩

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