map — Mathlib

English

The inclusion map S → A preserves addition: the sum in S maps to the sum in A under the inclusion.

Русский

Включение сохраняет сложение: сумма в S отображается как сумма в A.

LaTeX

$$$ (x+y)^{\\uparrow} = x^{\\uparrow} + y^{\\uparrow} \\quad (x,y \\in S). $$$

Lean4

/-- Transport a non-unital subalgebra via an algebra homomorphism. -/
def map (f : F) (S : NonUnitalSubalgebra R A) : NonUnitalSubalgebra R B :=
  { S.toNonUnitalSubsemiring.map (f : A →ₙ+* B) with
    smul_mem' := fun r b hb => by
      rcases hb with ⟨a, ha, rfl⟩
      exact map_smulₛₗ f r a ▸ Set.mem_image_of_mem f (S.smul_mem' r ha) }

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