comap — Mathlib

English

The preimage (comap) of a subalgebra T ⊆ B along an algebra homomorphism f: A → B is a subalgebra of A consisting of those a ∈ A with f(a) ∈ T.

Русский

Предобразование (comap) подалгебры T ⊆ B вдоль гомоморфизма f: A → B образует подалгебру в A, состоящую из таких a ∈ A, что f(a) ∈ T.

LaTeX

$$$\text{comap}(f,T) = \{ a \in A : f(a) \in T \}$$$

Lean4

/-- Preimage of a subalgebra under an algebra homomorphism. -/
@[simps! coe toSubsemiring]
def comap (f : A →ₐ[R] B) (S : Subalgebra R B) : Subalgebra R A :=
  { S.toSubsemiring.comap (f : A →+* B) with
    algebraMap_mem' := fun r => show f (algebraMap R A r) ∈ S from (f.commutes r).symm ▸ S.algebraMap_mem r }

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