toAlgHomClass — Mathlib

English

For any F in BialgHomClass, the map compatibility with comulAlgHom holds: (Algebra.TensorProduct.map f f) ∘ comulAlgHom_A = comulAlgHom_B ∘ f.

Русский

Для любого F в BialgHomClass выполняется совместимость map с comulAlgHom: (Algebra.TensorProduct.map f f) ∘ comulAlgHom_A = comulAlgHom_B ∘ f.

LaTeX

$$$((\\mathrm{AlgebraTensorProduct.map} f f) \\circ \\mathrm{comulAlgHom}\\;A) = \\mathrm{comulAlgHom}\\;B \\circ f$$$

Lean4

instance (priority := 100) toAlgHomClass : AlgHomClass F R A B
    where
  map_mul := map_mul
  map_one := map_one
  map_add := map_add
  map_zero := map_zero
  commutes := fun c r => by simp only [Algebra.algebraMap_eq_smul_one, map_smul, map_one]

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