ringHom_mem_submonoid_of_factors_subset_of_units_subset

English

If a ring homomorphism maps all factors of a to a submonoid and all units to that submonoid, then the image of a lies in the submonoid.

Русский

Если гомоморфизм колец отображает все факторы a в подмоноид, а все еденицы также в этот подмоноид, то образ a принадлежит подмоноиду.

LaTeX

$$$f\\ a \\in s$$$

Lean4

/-- If a `RingHom` maps all units and all factors of an element `a` into a submonoid `s`, then it
also maps `a` into that submonoid. -/
theorem ringHom_mem_submonoid_of_factors_subset_of_units_subset {R S : Type*} [CommRing R] [IsDomain R]
    [IsPrincipalIdealRing R] [NonAssocSemiring S] (f : R →+* S) (s : Submonoid S) (a : R) (ha : a ≠ 0)
    (h : ∀ b ∈ factors a, f b ∈ s) (hf : ∀ c : Rˣ, f c ∈ s) : f a ∈ s :=
  mem_submonoid_of_factors_subset_of_units_subset (s.comap f.toMonoidHom) ha h hf

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