comap — Mathlib

English

For a functor f and Submonoid S, the comap S under f has the underlying set equal to the preimage of S under f.

Русский

Для отображения f и подмонод S, прообраз comap S по f совпадает с предобразом S по f.

LaTeX

$$$ (S.org) = f^{-1}(S) $$$

Lean4

/-- The preimage of a submonoid along a monoid homomorphism is a submonoid. -/
@[to_additive /-- The preimage of an `AddSubmonoid` along an `AddMonoid` homomorphism is an `AddSubmonoid`. -/
    ]
def comap (f : F) (S : Submonoid N) : Submonoid M
    where
  carrier := f ⁻¹' S
  one_mem' := show f 1 ∈ S by rw [map_one]; exact S.one_mem
  mul_mem' ha hb := show f (_ * _) ∈ S by rw [map_mul]; exact S.mul_mem ha hb

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