submonoidComap_surjective_of_surjective

English

Let f: M →* N be a surjective monoid homomorphism and N' a submonoid of N. Then the preimage map f^{-1} with respect to N' is surjective onto Submonoid M; i.e., every Submonoid of M arises as the preimage of some Submonoid of N.

Русский

Пусть f: M →* N сюръективно, и N' — подмоноид N. Тогда отображение обратного образа ф с учётом N' сюръективно: любая подмонойд M является прообразом некоторого подмонойда N.

LaTeX

$$$ \forall S \in \mathrm{Submonoid}(M),\ \exists T \in \mathrm{Submonoid}(N),\ f\text{.submonoidComap}~T = S $$$

Lean4

@[to_additive]
theorem submonoidComap_surjective_of_surjective (f : M →* N) (N' : Submonoid N) (hf : Surjective f) :
    Surjective (f.submonoidComap N') := fun y ↦ by
  obtain ⟨x, hx⟩ := hf y
  use ⟨x, mem_comap.mpr (hx ▸ y.2)⟩
  apply Subtype.val_injective
  simp [hx]

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