compContinuousMap_id — Mathlib

English

The composition map with the identity morphism acts as the identity on spectra.

Русский

Композиция с тождественным гомоморфизмом действует как тождественный отображение на спектрах.

LaTeX

$$$compContinuousMap(\\\\mathrm{id}_{A}) = \\\\mathrm{id}_{CharacterSpace_{𝕜} A}$$$

Lean4

/-- `WeakDual.CharacterSpace.compContinuousMap` sends the identity to the identity. -/
@[simp]
theorem compContinuousMap_id : compContinuousMap (StarAlgHom.id 𝕜 A) = ContinuousMap.id (characterSpace 𝕜 A) :=
  ContinuousMap.ext fun _a => ext fun _x => rfl

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