comap — Mathlib

English

The preimage of a subring along a ring homomorphism is a subring.

Русский

Предобраз подполья по кольцевому гомоморфизму образует подполье.

LaTeX

$$$\\forall f:\\ R \\to^+_* S\\, (s: Subring S)\\Rightarrow (s.comap f) \\text{ is a Subring of } R.$$$

Lean4

/-- The preimage of a subring along a ring homomorphism is a subring. -/
def comap {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) (s : Subring S) : Subring R :=
  { s.toSubmonoid.comap (f : R →* S), s.toAddSubgroup.comap (f : R →+ S) with carrier := f ⁻¹' s.carrier }

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