English
For A,B in (Mon (CommAlgCat R)ᵒᵖ) with morphism f, the inverse map preserves monoid structure via AlgHom underlying f.hom.
Русский
Для A,B в (Mon (CommAlgCat R)ᵒᵖ) с морфизмом f сохранение моноидной структуры через AlgHom (фундаментальный).
LaTeX
$$$\\text{commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom }(f)$$$
Lean4
/-- The `G` representation `C(G, rep)` given a representation `rep`.
The `G` action is defined by `g • f := x ↦ g • f (g⁻¹ * x)`. -/
abbrev Iobj (rep : Action (TopModuleCat R) G) : Action (TopModuleCat R) G
where
V := .of R C(G, rep.V)
ρ :=
{ toFun
g :=
TopModuleCat.ofHom
{ toFun f := .comp (rep.ρ g).hom (f.comp (Homeomorph.mulLeft g⁻¹))
map_add' _ _ := by ext; simp
map_smul' _ _ := by ext; simp
cont := (continuous_postcomp _).comp (continuous_precomp _) }
map_one' := ConcreteCategory.ext (by ext; simp)
map_mul' _ _ := ConcreteCategory.ext (by ext; simp [mul_assoc]) }
