Lift of MonoidHom M N to MonoidHom (SeparationQuotient M) N

In this file we define the lift of a continuous monoid homomorphism f from M to N to SeparationQuotient M, assuming that f maps two inseparable elements to the same element.

noncomputable def SeparationQuotient.liftContinuousMonoidHom {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [CommMonoid M] [ContinuousMul M] [CommMonoid N] (f : ContinuousMonoidHom M N) (hf : ∀ (x y : M), Inseparable x y → f x = f y) : ContinuousMonoidHom (SeparationQuotient M) N

The lift of a monoid hom from M to a monoid hom from SeparationQuotient M.

Equations

• SeparationQuotient.liftContinuousMonoidHom f hf = { toFun := SeparationQuotient.lift (⇑f) hf, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

noncomputable def SeparationQuotient.liftContinuousAddMonoidHom {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [AddCommMonoid M] [ContinuousAdd M] [AddCommMonoid N] (f : ContinuousAddMonoidHom M N) (hf : ∀ (x y : M), Inseparable x y → f x = f y) : ContinuousAddMonoidHom (SeparationQuotient M) N

The lift of an additive monoid hom from M to an additive monoid hom from SeparationQuotient M.

Equations

• SeparationQuotient.liftContinuousAddMonoidHom f hf = { toFun := SeparationQuotient.lift (⇑f) hf, map_zero' := ⋯, map_add' := ⋯, continuous_toFun := ⋯ }

@[simp]

theorem SeparationQuotient.liftContinuousCommMonoidHom_mk {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [CommMonoid M] [ContinuousMul M] [CommMonoid N] (f : ContinuousMonoidHom M N) (hf : ∀ (x y : M), Inseparable x y → f x = f y) (x : M) : (liftContinuousMonoidHom f hf) (mk x) = f x

@[simp]

theorem SeparationQuotient.liftContinuousAddCommMonoidHom_mk {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [AddCommMonoid M] [ContinuousAdd M] [AddCommMonoid N] (f : ContinuousAddMonoidHom M N) (hf : ∀ (x y : M), Inseparable x y → f x = f y) (x : M) : (liftContinuousAddMonoidHom f hf) (mk x) = f x