NYLL
Module

TopologicalAbelianizationQuotientFaithfulness.lean

Nyll.ProCGroups.Abelian.TopologicalAbelianizationQuotientFaithfulness
2 declarations indexed from sourceView source ↗

Module documentation

Faithfulness pulled back from quotient abelianizations

Trivial conjugation descends along a continuous homomorphism. Consequently, faithfulness on the image pulls back for normal subgroups containing its kernel.

Imports1
Imported by2

Declarations

theorem

quotientConjugationTopologicalAbelianizationMap_mk_eq_one_map

L25 ↗
ProCGroups.Abelian.quotientConjugationTopologicalAbelianizationMap_mk_eq_one_map
Documentation

Trivial conjugation on a normal subgroup's topological abelianization remains trivial on its image under a continuous homomorphism.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Abelian
variable {G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
  [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
  (f : G →ₜ* H) (N : Subgroup G) [N.Normal] [(N.map f.toMonoidHom).Normal]
Lean source · statement
theorem quotientConjugationTopologicalAbelianizationMap_mk_eq_one_map
    (g : G)
    (hg : quotientConjugationTopologicalAbelianizationMap N (QuotientGroup.mk' N g) = 1) :
    quotientConjugationTopologicalAbelianizationMap (N.map f.toMonoidHom)
      (QuotientGroup.mk' (N.map f.toMonoidHom) (f g)) = 1
theorem

quotientConjugationTopologicalAbelianizationMap_injective_of_map

L60 ↗
ProCGroups.Abelian.quotientConjugationTopologicalAbelianizationMap_injective_of_map
Documentation

Faithfulness on the image of a normal subgroup pulls back when the subgroup contains the kernel of the ambient continuous homomorphism.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Abelian
variable {G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
  [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
  (f : G →ₜ* H) (N : Subgroup G) [N.Normal] [(N.map f.toMonoidHom).Normal]
Lean source · statement
theorem quotientConjugationTopologicalAbelianizationMap_injective_of_map
    (hker : f.toMonoidHom.ker ≤ N)
    (hinj : Function.Injective
      (quotientConjugationTopologicalAbelianizationMap (N.map f.toMonoidHom))) :
    Function.Injective (quotientConjugationTopologicalAbelianizationMap N)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.