English
There is an equivalence between continuous maps from X to the group of units of a monoid M and the group of units of the monoid of continuous maps X → M.
Русский
Существуют эквивалентности между непрерывными отображениями из X в группу единиц моноида M и еденицами моноида непрерывных отображений X → M.
LaTeX
$$$C(X, M^{\times}) \simeq C(X, M)^{\times}.$$$
Lean4
/-- Equivalence between continuous maps into the units of a monoid with continuous multiplication
and the units of the monoid of continuous maps. -/
-- `simps` generates some lemmas here with LHS not in simp normal form,
-- so we write them out manually below.
@[to_additive (attr := simps apply_val_apply symm_apply_apply_val) /--
Equivalence between continuous maps into the additive units of an additive monoid with
continuous addition and the additive units of the additive monoid of continuous maps. -/
]
def unitsLift : C(X, Mˣ) ≃ C(X, M)ˣ
where
toFun
f :=
{ val := ⟨fun x => f x, Units.continuous_val.comp f.continuous⟩
inv := ⟨fun x => ↑(f x)⁻¹, Units.continuous_val.comp (continuous_inv.comp f.continuous)⟩
val_inv := ext fun _ => Units.mul_inv _
inv_val := ext fun _ => Units.inv_mul _ }
invFun
f :=
{ toFun := fun x =>
⟨(f : C(X, M)) x, (↑f⁻¹ : C(X, M)) x, ContinuousMap.congr_fun f.mul_inv x, ContinuousMap.congr_fun f.inv_mul x⟩
continuous_toFun :=
continuous_induced_rng.2 <|
(f : C(X, M)).continuous.prodMk <| MulOpposite.continuous_op.comp (↑f⁻¹ : C(X, M)).continuous }
