Continuity of homomorphisms and maps involving subgroups and quotients

Mathlib's Subgroup.subtype and QuotientGroup.mk' are bare MonoidHoms, and its coercion ContinuousMonoidHom.toContinuousMonoidHom applies only to bundled types that already carry a ContinuousMapClass instance, so neither map is available as a ContinuousMonoidHom. This file packages those maps for a topological group and the subspace and quotient topologies. It also provides inverse conjugation n ↦ g⁻¹ * n * g on a normal subgroup, together with its evaluation, identity, and composition laws, and the continuous lift through a quotient by a normal subgroup. Named compatibility proofs describe subgroup inclusions and composition of scalar/coefficient maps for pullbacks of cochains; composition uses Mathlib's semiconjugacy API. A homomorphism from a topological group with open kernel is also continuous, for every topology on the target. The projections of a product of topological monoids onto its factors are packaged as ContinuousMonoidHom.proj, next to Mathlib's ContinuousMonoidHom.fst and ContinuousMonoidHom.snd. Integer powers of continuous homomorphisms into a commutative topological group are computed pointwise, and the multiplicative isomorphism underlying a continuous multiplicative isomorphism has the same underlying function. A topologically embedded continuous group homomorphism is also packaged as a continuous multiplicative equivalence with its range, with forward and inverse computation rules. The file also records the pointwise characterization of finite-order continuous homomorphisms and the open kernel of a finite-order continuous character into complex units. Kernels of continuous homomorphisms into a T1 monoid are closed, so on a compact group the common kernel of a family of them is approximated from outside by the common kernels of its finite subfamilies, and the range of a continuous homomorphism out of a compact group into a Hausdorff group is a closed subgroup.

theorem ContinuousMonoidHom.eq_one_of_isMulTorsionFree {A : Type u_2} {B : Type u_3} [Monoid A] [TopologicalSpace A] [CompactSpace A] [LeftCancelMonoid B] [TopologicalSpace B] [DiscreteTopology B] [IsMulTorsionFree B] (f : A →ₜ* B) : f = 1

A continuous homomorphism from a compact monoid to a discrete torsion-free left-cancellative monoid is trivial: its image is finite, hence consists of finite-order elements.

theorem ContinuousAddMonoidHom.eq_zero_of_isAddTorsionFree {A : Type u_2} {B : Type u_3} [AddMonoid A] [TopologicalSpace A] [CompactSpace A] [AddLeftCancelMonoid B] [TopologicalSpace B] [DiscreteTopology B] [IsAddTorsionFree B] (f : A →ₜ+ B) : f = 0

A continuous additive homomorphism from a compact additive monoid to a discrete torsion-free left-cancellative additive monoid is zero: its image is finite.

theorem ContinuousMonoidHom.isOfFinOrder_iff_exists_pow_apply_eq_one {A : Type u_2} {B : Type u_3} [Monoid A] [TopologicalSpace A] [CommGroup B] [TopologicalSpace B] [IsTopologicalGroup B] (f : A →ₜ* B) : IsOfFinOrder f ↔ ∃ (n : ℕ), 0 < n ∧ ∀ (x : A), f x ^ n = 1

A continuous homomorphism into a commutative topological group has finite order exactly when all its values have a common positive exponent equal to one.

theorem ContinuousMonoidHom.isOpen_ker_of_isOfFinOrder {M : Type u_2} [Monoid M] [TopologicalSpace M] {χ : M →ₜ* ℂˣ} (hχ : IsOfFinOrder χ) : IsOpen (⇑χ ⁻¹' {1})

A finite-order continuous character into the complex units has open kernel.

theorem MonoidHom.continuous_of_isOpen_ker {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {F : Type u_2} [MulOneClass F] [TopologicalSpace F] (f : G →* F) (hf : IsOpen ↑f.ker) : Continuous ⇑f

A homomorphism with open kernel out of a group with continuous translations is continuous for every topology on the target: it is constant on the open coset x * ker f of each point x.

theorem ContinuousMonoidHom.isClosed_ker {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Monoid H] [TopologicalSpace H] [T1Space H] (φ : G →ₜ* H) : IsClosed ↑φ.ker

The kernel of a continuous homomorphism into a T1 monoid is closed: it is the preimage of the closed point 1.

theorem TauCeti.exists_finset_iInter_ker_subset {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] {H : Type u_2} [Monoid H] [TopologicalSpace H] [T1Space H] {ι : Type u_3} (φ : ι → G →ₜ* H) {U : Set G} (hU : IsOpen U) (h : ⋂ (j : ι), ↑(φ j).ker ⊆ U) : ∃ (F : Finset ι), ⋂ j ∈ F, ↑(φ j).ker ⊆ U

A finite subfamily of kernels suffices. In a compact group, an open set containing the common kernel of a family of continuous homomorphisms into a T1 monoid already contains the common kernel of a finite subfamily: each kernel is closed, so this is the finite intersection property.

theorem MonoidHom.isClosed_range_of_continuous {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] [T2Space H] {f : G →* H} (hf : Continuous ⇑f) : IsClosed ↑f.range

The range of a continuous homomorphism out of a compact group into a Hausdorff group is a closed subgroup.

theorem ContinuousMonoidHom.comp_map_smul {A : Type u_2} {B : Type u_3} {C : Type u_4} {M : Type u_5} {N : Type u_6} {P : Type u_7} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [AddZero M] [AddZero N] [AddZero P] [SMul A M] [SMul B N] [SMul C P] (φ : B →ₜ* A) (ψ : C →ₜ* B) (f : M →+ N) (q : N →+ P) (hf : ∀ (b : B) (m : M), f (φ b • m) = b • f m) (hq : ∀ (c : C) (n : N), q (ψ c • n) = c • q n) (c : C) (m : M) : (q.comp f) ((φ.comp ψ) c • m) = c • (q.comp f) m

Compatible coefficient maps compose along continuous scalar homomorphisms. This supplies the compatibility hypothesis of the composite pair (φ.comp ψ, q.comp f) in cochain pullbacks.

@[simp]

theorem ContinuousMonoidHom.coe_mk {A : Type u_2} {B : Type u_3} [Monoid A] [TopologicalSpace A] [Monoid B] [TopologicalSpace B] (f : A →* B) (hf : Continuous ⇑f) : ⇑{ toMonoidHom := f, continuous_toFun := hf } = ⇑f

Evaluating a continuous homomorphism assembled from a homomorphism and a continuity proof.

def ContinuousMonoidHom.proj {ι : Type u_2} {A : ι → Type u_3} [(i : ι) → Monoid (A i)] [(i : ι) → TopologicalSpace (A i)] (i : ι) : ((i : ι) → A i) →ₜ* A i

The projection of a product ∀ i, A i of topological monoids onto its i-th factor, as a continuous homomorphism. This is the analogue for products of ContinuousMonoidHom.fst and ContinuousMonoidHom.snd.

Equations

• ContinuousMonoidHom.proj i = { toMonoidHom := Pi.evalMonoidHom A i, continuous_toFun := ⋯ }

def ContinuousAddMonoidHom.proj {ι : Type u_2} {A : ι → Type u_3} [(i : ι) → AddMonoid (A i)] [(i : ι) → TopologicalSpace (A i)] (i : ι) : ((i : ι) → A i) →ₜ+ A i

The projection of a product ∀ i, A i of topological additive monoids onto its i-th factor, as a continuous additive homomorphism. This is the analogue for products of ContinuousAddMonoidHom.fst and ContinuousAddMonoidHom.snd.

Equations

• ContinuousAddMonoidHom.proj i = { toAddMonoidHom := Pi.evalAddMonoidHom A i, continuous_toFun := ⋯ }

@[simp]

theorem ContinuousMonoidHom.proj_apply {ι : Type u_2} {A : ι → Type u_3} [(i : ι) → Monoid (A i)] [(i : ι) → TopologicalSpace (A i)] (i : ι) (f : (i : ι) → A i) : (proj i) f = f i

The projection onto the i-th factor evaluates a function at i.

@[simp]

theorem ContinuousAddMonoidHom.proj_apply {ι : Type u_2} {A : ι → Type u_3} [(i : ι) → AddMonoid (A i)] [(i : ι) → TopologicalSpace (A i)] (i : ι) (f : (i : ι) → A i) : (proj i) f = f i

The projection onto the i-th factor evaluates a function at i.

@[simp]

theorem ContinuousMulEquiv.coe_toMulEquiv {A : Type u_2} {B : Type u_3} [Mul A] [TopologicalSpace A] [Mul B] [TopologicalSpace B] (f : A ≃ₜ* B) : ⇑↑f = ⇑f

The multiplicative isomorphism underlying a continuous multiplicative isomorphism has the same underlying function. This is the ContinuousMulEquiv analogue of RingEquiv.coe_toMulEquiv.

@[simp]

theorem ContinuousAddEquiv.coe_toAddEquiv {A : Type u_2} {B : Type u_3} [Add A] [TopologicalSpace A] [Add B] [TopologicalSpace B] (f : A ≃ₜ+ B) : ⇑↑f = ⇑f

The additive isomorphism underlying a continuous additive isomorphism has the same underlying function.

noncomputable def ContinuousMonoidHom.equivRangeOfIsEmbedding {A : Type u_2} {B : Type u_3} [Group A] [Group B] [TopologicalSpace A] [TopologicalSpace B] (f : A →ₜ* B) (hf : Topology.IsEmbedding ⇑f) : A ≃ₜ* ↥(↑f).range

A topologically embedded continuous group homomorphism is continuously multiplicatively equivalent to its range.

Equations

• f.equivRangeOfIsEmbedding hf = ContinuousMulEquiv.mk' hf.toHomeomorph ⋯

@[simp]

theorem ContinuousMonoidHom.equivRangeOfIsEmbedding_apply {A : Type u_2} {B : Type u_3} [Group A] [Group B] [TopologicalSpace A] [TopologicalSpace B] (f : A →ₜ* B) (hf : Topology.IsEmbedding ⇑f) (x : A) : (f.equivRangeOfIsEmbedding hf) x = ⟨f x, ⋯⟩

The equivalence with the range sends an element to its canonical range representative.

@[simp]

theorem ContinuousMonoidHom.equivRangeOfIsEmbedding_symm_apply {A : Type u_2} {B : Type u_3} [Group A] [Group B] [TopologicalSpace A] [TopologicalSpace B] (f : A →ₜ* B) (hf : Topology.IsEmbedding ⇑f) (x : A) : (f.equivRangeOfIsEmbedding hf).symm ⟨f x, ⋯⟩ = x

The inverse equivalence sends a canonical range representative back to its source.

@[simp]

theorem ContinuousMonoidHom.zpow_apply {A : Type u_2} {E : Type u_3} [Monoid A] [TopologicalSpace A] [CommGroup E] [TopologicalSpace E] [IsTopologicalGroup E] (f : A →ₜ* E) (n : ℤ) (a : A) : (f ^ n) a = f a ^ n

Integer powers of continuous homomorphisms into a commutative topological group are computed pointwise.

def TauCeti.ContinuousMonoidHom.subgroupSubtype {G : Type u_1} [Group G] [TopologicalSpace G] (S : Subgroup G) : ↥S →ₜ* G

The inclusion of a subgroup, carrying the subspace topology, as a continuous homomorphism.

Equations

• TauCeti.ContinuousMonoidHom.subgroupSubtype S = { toMonoidHom := S.subtype, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.ContinuousMonoidHom.coe_subgroupSubtype {G : Type u_1} [Group G] [TopologicalSpace G] (S : Subgroup G) : ↑(subgroupSubtype S) = S.subtype

@[simp]

theorem TauCeti.ContinuousMonoidHom.subgroupSubtype_apply {G : Type u_1} [Group G] [TopologicalSpace G] (S : Subgroup G) (s : ↥S) : (subgroupSubtype S) s = ↑s

theorem TauCeti.ContinuousMonoidHom.id_subgroupSubtype_smul {G : Type u_1} [Group G] [TopologicalSpace G] (M : Type u_2) [AddZero M] [SMul G M] (S : Subgroup G) (s : ↥S) (m : M) : (AddMonoidHom.id M) ((subgroupSubtype S) s • m) = s • (AddMonoidHom.id M) m

The identity coefficient map is compatible with the continuous inclusion of a subgroup.

def TauCeti.ContinuousMonoidHom.subgroupInclusion {G : Type u_1} [Group G] [TopologicalSpace G] {H S : Subgroup G} (h : H ≤ S) : ↥H →ₜ* ↥S

The inclusion of a subgroup into a larger subgroup, both carrying the subspace topology, as a continuous homomorphism.

Equations

• TauCeti.ContinuousMonoidHom.subgroupInclusion h = { toMonoidHom := Subgroup.inclusion h, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.ContinuousMonoidHom.coe_subgroupInclusion {G : Type u_1} [Group G] [TopologicalSpace G] {H S : Subgroup G} (h : H ≤ S) : ↑(subgroupInclusion h) = Subgroup.inclusion h

@[simp]

theorem TauCeti.ContinuousMonoidHom.subgroupInclusion_apply {G : Type u_1} [Group G] [TopologicalSpace G] {H S : Subgroup G} (h : H ≤ S) (x : ↥H) : (subgroupInclusion h) x = (Subgroup.inclusion h) x

@[simp]

theorem TauCeti.ContinuousMonoidHom.subgroupInclusion_refl {G : Type u_1} [Group G] [TopologicalSpace G] (H : Subgroup G) : subgroupInclusion ⋯ = ContinuousMonoidHom.id ↥H

The inclusion of a subgroup into itself is the identity.

@[simp]

theorem TauCeti.ContinuousMonoidHom.subgroupInclusion_comp_subgroupInclusion {G : Type u_1} [Group G] [TopologicalSpace G] {H S T : Subgroup G} (hHS : H ≤ S) (hST : S ≤ T) : (subgroupInclusion hST).comp (subgroupInclusion hHS) = subgroupInclusion ⋯

Inclusions of subgroups compose: including H into S and then S into T is including H into T.

@[simp]

theorem TauCeti.ContinuousMonoidHom.subgroupSubtype_comp_subgroupInclusion {G : Type u_1} [Group G] [TopologicalSpace G] {H S : Subgroup G} (h : H ≤ S) : (subgroupSubtype S).comp (subgroupInclusion h) = subgroupSubtype H

The inclusion of a subgroup factors through any larger subgroup.

def Subgroup.inverseConjugationHom {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (g : G) : ↥N →ₜ* ↥N

The inverse conjugation homomorphism of a normal subgroup, with the subspace topology.

Equations

• N.inverseConjugationHom g = { toMonoidHom := MulEquiv.toMonoidHom (MulAut.conjNormal g⁻¹), continuous_toFun := ⋯ }

@[simp]

theorem Subgroup.inverseConjugationHom_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (g : G) (n : ↥N) : (N.inverseConjugationHom g) n = ⟨g⁻¹ * ↑n * g, ⋯⟩

Evaluation of inverse conjugation on a subgroup element.

@[simp]

theorem Subgroup.inverseConjugationHom_one {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] : N.inverseConjugationHom 1 = ContinuousMonoidHom.id ↥N

Inverse conjugation by the identity is the identity continuous homomorphism.

@[simp]

theorem Subgroup.inverseConjugationHom_mul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (g h : G) : N.inverseConjugationHom (g * h) = (N.inverseConjugationHom h).comp (N.inverseConjugationHom g)

Inverse conjugation by a product is the reversed composition of inverse conjugations.

def TauCeti.ContinuousMonoidHom.quotientMk {G : Type u_1} [Group G] [TopologicalSpace G] (N : Subgroup G) [N.Normal] : G →ₜ* G ⧸ N

The projection onto the quotient by a normal subgroup, carrying the quotient topology, as a continuous homomorphism.

Equations

• TauCeti.ContinuousMonoidHom.quotientMk N = { toMonoidHom := QuotientGroup.mk' N, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.ContinuousMonoidHom.coe_quotientMk {G : Type u_1} [Group G] [TopologicalSpace G] (N : Subgroup G) [N.Normal] : ↑(quotientMk N) = QuotientGroup.mk' N

@[simp]

theorem TauCeti.ContinuousMonoidHom.quotientMk_apply {G : Type u_1} [Group G] [TopologicalSpace G] (N : Subgroup G) [N.Normal] (g : G) : (quotientMk N) g = ↑g

def TauCeti.ContinuousMonoidHom.quotientLift {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Monoid H] [TopologicalSpace H] (N : Subgroup G) [N.Normal] (f : G →ₜ* H) (hf : N ≤ f.ker) : G ⧸ N →ₜ* H

The continuous homomorphism induced on a quotient by a continuous homomorphism that kills the normal subgroup.

Equations

• TauCeti.ContinuousMonoidHom.quotientLift N f hf = { toMonoidHom := QuotientGroup.lift N f.toMonoidHom hf, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.ContinuousMonoidHom.coe_quotientLift {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Monoid H] [TopologicalSpace H] (N : Subgroup G) [N.Normal] (f : G →ₜ* H) (hf : N ≤ f.ker) : ↑(quotientLift N f hf) = QuotientGroup.lift N f.toMonoidHom hf

@[simp]

theorem TauCeti.ContinuousMonoidHom.quotientLift_mk {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Monoid H] [TopologicalSpace H] (N : Subgroup G) [N.Normal] (f : G →ₜ* H) (hf : N ≤ f.ker) (x : G) : (quotientLift N f hf) ↑x = f x

Evaluation of the quotient lift on a class represented by x.

@[simp]

theorem TauCeti.ContinuousMonoidHom.quotientLift_comp_quotientMk {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Monoid H] [TopologicalSpace H] (N : Subgroup G) [N.Normal] (f : G →ₜ* H) (hf : N ≤ f.ker) : (quotientLift N f hf).comp (quotientMk N) = f

Composition of the quotient lift with the quotient projection recovers the original map.

theorem TauCeti.ContinuousMonoidHom.quotientLift_unique {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Monoid H] [TopologicalSpace H] (N : Subgroup G) [N.Normal] (f : G →ₜ* H) (hf : N ≤ f.ker) (g : G ⧸ N →ₜ* H) (hg : ∀ (x : G), g ↑x = f x) : g = quotientLift N f hf

A continuous homomorphism on the quotient is determined by its values on representatives.

theorem TauCeti.ContinuousMonoidHom.le_ker_comp_quotientMk {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Monoid H] [TopologicalSpace H] (N : Subgroup G) [N.Normal] (g : G ⧸ N →ₜ* H) : N ≤ (↑(g.comp (quotientMk N))).ker

The kernel of precomposition with the quotient projection contains the subgroup.

def TauCeti.ContinuousMonoidHom.quotientHomEquiv {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Monoid H] [TopologicalSpace H] (N : Subgroup G) [N.Normal] : (G ⧸ N →ₜ* H) ≃ { f : G →ₜ* H // N ≤ (↑f).ker }

Precomposition with the quotient projection identifies continuous homomorphisms on the quotient with continuous homomorphisms whose kernels contain the normal subgroup.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ContinuousMonoidHom.quotientHomEquiv_apply_coe {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Monoid H] [TopologicalSpace H] (N : Subgroup G) [N.Normal] (g : G ⧸ N →ₜ* H) : ↑((quotientHomEquiv N) g) = g.comp (quotientMk N)

Evaluation of the forward quotient homomorphism equivalence.

@[simp]

theorem TauCeti.ContinuousMonoidHom.quotientHomEquiv_symm_apply {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Monoid H] [TopologicalSpace H] (N : Subgroup G) [N.Normal] (f : { f : G →ₜ* H // N ≤ (↑f).ker }) : (quotientHomEquiv N).symm f = quotientLift N ↑f ⋯

Evaluation of the inverse quotient homomorphism equivalence.