English
There exists a continuous linear map f such that mkCLM ∘ f = id on SeparationQuotient, realized via an inverse of mk restricted to the quotient.
Русский
Существует непрерывное линейное отображение f, такое что mkCLM ∘ f = id на SeparationQuotient, реализованное через частный обратный к mk.
LaTeX
$$$\exists f: SeparationQuotient E \to_L[K] E, mkCLM K E \circ_L f = \mathrm{id}$$$
Lean4
/-- The lift of a monoid hom from `M` to a monoid hom from `SeparationQuotient M`. -/
@[to_additive /-- The lift of an additive monoid hom from `M` to an additive monoid hom from
`SeparationQuotient M`. -/
]
noncomputable def liftContinuousMonoidHom [CommMonoid M] [ContinuousMul M] [CommMonoid N] (f : ContinuousMonoidHom M N)
(hf : ∀ x y, Inseparable x y → f x = f y) : ContinuousMonoidHom (SeparationQuotient M) N
where
toFun := SeparationQuotient.lift f hf
map_one' := map_one f
map_mul' := Quotient.ind₂ <| map_mul f
continuous_toFun := SeparationQuotient.continuous_lift.mpr f.2
