ProCGroups.ProC.Category.Basic

11 Theorem | 9 Definition | 3 Abbreviation | 2 Structure | 15 Instance

This module studies basic for pro cgroups. The category of pro-\(C\) groups for a fixed topological pro-\(C\) predicate. The category object coerces to its underlying type.

Open this file on GitHub

import

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProCGroups.ProC.Subgroups.Closed
ProCGroups.Profinite.MathlibBridge

Imported by

Structure ProCGrp GitHub

structure ProCGrp (ProC : ProCGroups.ProC.ProCGroupPredicate.{u}) where
  /-- The underlying Mathlib profinite group. -/
  toProfiniteGrp : ProfiniteGrp.{u}
  /-- The pro-`C` structure on the underlying profinite group. -/

The category of pro-\(C\) groups for a fixed topological pro-\(C\) predicate.

Instance ProCGrp.instCoeSort GitHub

instance instCoeSort : CoeSort (ProCGrp ProC) (Type u) where
  coe G := G.toProfiniteGrp

The category object coerces to its underlying type.

Instance ProCGrp.instGroup GitHub

instance instGroup (G : ProCGrp ProC) : Group G :=
  inferInstanceAs (Group G.toProfiniteGrp)

The constructed carrier inherits its group structure from the coordinatewise group structure of the construction.

Instance ProCGrp.instTopologicalSpace GitHub

instance instTopologicalSpace (G : ProCGrp ProC) : TopologicalSpace G :=
  inferInstanceAs (TopologicalSpace G.toProfiniteGrp)

The constructed object carries the topological space structure inherited from its construction.

Instance ProCGrp.instIsTopologicalGroup GitHub

instance instIsTopologicalGroup (G : ProCGrp ProC) : IsTopologicalGroup G :=
  inferInstanceAs (IsTopologicalGroup G.toProfiniteGrp)

The object is a topological group with the induced group operations and topology.

Instance ProCGrp.instCompactSpace GitHub

instance instCompactSpace (G : ProCGrp ProC) : CompactSpace G :=
  inferInstanceAs (CompactSpace G.toProfiniteGrp)

The constructed object carries the compact space structure inherited from its profinite construction.

Instance ProCGrp.instT2Space GitHub

instance instT2Space (G : ProCGrp ProC) : T2Space G :=
  inferInstanceAs (T2Space G.toProfiniteGrp)

The constructed object is Hausdorff, with its \(T_2\) structure inherited from the profinite construction.

Instance ProCGrp.instTotallyDisconnectedSpace GitHub

instance instTotallyDisconnectedSpace (G : ProCGrp ProC) : TotallyDisconnectedSpace G :=
  inferInstanceAs (TotallyDisconnectedSpace G.toProfiniteGrp)

The constructed object carries the totally disconnected space structure inherited from its profinite construction.

Instance ProCGrp.instProCGroup GitHub

instance instProCGroup (G : ProCGrp ProC) : ProCGroups.ProC.ProCGroup ProC G :=
  inferInstanceAs (ProCGroups.ProC.ProCGroup ProC G.toProfiniteGrp)

The object satisfies the pro-\(C\) group condition.

Abbreviation ProCGrp.of GitHub

abbrev of (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [ProCGroups.ProC.ProCGroup ProC G] : ProCGrp ProC where
  toProfiniteGrp := by
    letI : CompactSpace G := ProCGroups.ProC.ProCGroup.compactSpace ProC G
    letI : TotallyDisconnectedSpace G :=
      ProCGroups.ProC.ProCGroup.totallyDisconnectedSpace ProC G
    exact ProfiniteGrp.of G
  proCGroup := inferInstance

This declaration constructs a bundled pro-\(C\) group from an unbundled topological group with a pro-\(C\)-group instance.

Theorem ProCGrp.coe_of GitHub

@[simp] theorem coe_of (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [ProCGroups.ProC.ProCGroup ProC G] :
    (of ProC G : Type u) = G

The carrier of the bundled pro-\(C\) group is the original type.

Show proof

Structure ProCGrp.Hom GitHub

structure Hom (A B : ProCGrp ProC) where
  /-- The underlying continuous monoid homomorphism. -/
  hom' : A →ₜ* B

Morphisms in \(\mathrm{ProCGrp}\) are continuous homomorphisms between the underlying bundled pro-\(C\) groups.

Instance ProCGrp.instCategory GitHub

instance instCategory : Category (ProCGrp ProC) where
  Hom A B := Hom A B
  id A := ⟨ContinuousMonoidHom.id A⟩
  comp f g := ⟨g.hom'.comp f.hom'⟩

Pro-\(C\) groups form a category.

Instance ProCGrp.instConcreteCategory GitHub

instance instConcreteCategory : ConcreteCategory (ProCGrp ProC) (fun X Y => X →ₜ* Y) where
  hom f := f.hom'
  ofHom f := ⟨f⟩

The category of pro-\(C\) groups has the concrete category structure inherited from its underlying type.

Abbreviation ProCGrp.Hom.hom GitHub

abbrev Hom.hom {A B : ProCGrp ProC} (f : A ⟶ B) : A →ₜ* B :=
  ConcreteCategory.hom (C := ProCGrp ProC) f

The underlying continuous homomorphism of a morphism.

Instance ProCGrp.instCoeFunHom GitHub

instance instCoeFunHom {A B : ProCGrp ProC} : CoeFun (A ⟶ B) (fun _ => A → B) where
  coe f := f.hom

A morphism coerces to its underlying continuous homomorphism.

Theorem ProCGrp.hom_id GitHub

@[simp] theorem hom_id {A : ProCGrp ProC} :
    (𝟙 A : A ⟶ A).hom = ContinuousMonoidHom.id A

The underlying homomorphism of the identity morphism is the identity continuous homomorphism.

Show proof

Theorem ProCGrp.id_apply GitHub

@[simp] theorem id_apply (A : ProCGrp ProC) (a : A) :
    (𝟙 A : A ⟶ A) a = a

The map is evaluated on an element by its defining coordinate formula.

Show proof

Theorem ProCGrp.hom_comp GitHub

@[simp] theorem hom_comp {A B C : ProCGrp ProC} (f : A ⟶ B) (g : B ⟶ C) :
    (f ≫ g).hom = g.hom.comp f.hom

The underlying homomorphism of a composite is the composite of underlying homomorphisms.

Show proof

Theorem ProCGrp.comp_apply GitHub

@[simp] theorem comp_apply {A B C : ProCGrp ProC} (f : A ⟶ B) (g : B ⟶ C) (a : A) :
    (f ≫ g) a = g (f a)

The composite map is computed pointwise by applying the constituent coordinate formulas in succession.

Show proof

Theorem ProCGrp.hom_ext GitHub

@[ext] theorem hom_ext {A B : ProCGrp ProC} {f g : A ⟶ B} (hf : f.hom = g.hom) :
    f = g

Morphisms in ProCGrp are equal when their underlying continuous homomorphisms are equal.

Show proof

Abbreviation ProCGrp.ofHom GitHub

abbrev ofHom {X Y : Type u}
    [Group X] [TopologicalSpace X] [IsTopologicalGroup X]
    [ProCGroups.ProC.ProCGroup ProC X]
    [Group Y] [TopologicalSpace Y] [IsTopologicalGroup Y]
    [ProCGroups.ProC.ProCGroup ProC Y]
    (f : X →ₜ* Y) : of ProC X ⟶ of ProC Y :=
  ConcreteCategory.ofHom f

Bundle a continuous monoid homomorphism as a morphism in \(\mathrm{ProCGrp}\).

Theorem ProCGrp.hom_ofHom GitHub

@[simp] theorem hom_ofHom {X Y : Type u}
    [Group X] [TopologicalSpace X] [IsTopologicalGroup X]
    [ProCGroups.ProC.ProCGroup ProC X]
    [Group Y] [TopologicalSpace Y] [IsTopologicalGroup Y]
    [ProCGroups.ProC.ProCGroup ProC Y]
    (f : X →ₜ* Y) : (ofHom (ProC := ProC) f).hom = f

The \(\mathrm{ofHom}\) constructor has the prescribed underlying continuous homomorphism.

Show proof

Theorem ProCGrp.ofHom_hom GitHub

@[simp] theorem ofHom_hom {A B : ProCGrp ProC} (f : A ⟶ B) :
    ConcreteCategory.ofHom (C := ProCGrp ProC) f.hom = f

Reconstructing a morphism from its underlying continuous homomorphism gives the original morphism.

Show proof

Theorem ProCGrp.ofHom_id GitHub

@[simp] theorem ofHom_id {X : Type u}
    [Group X] [TopologicalSpace X] [IsTopologicalGroup X]
    [ProCGroups.ProC.ProCGroup ProC X] :
    ofHom (ProC := ProC) (ContinuousMonoidHom.id X) = 𝟙 (of ProC X)

\(\mathrm{ofHom}\) sends the identity continuous homomorphism to the identity morphism.

Show proof

Theorem ProCGrp.ofHom_comp GitHub

@[simp] theorem ofHom_comp {X Y Z : Type u}
    [Group X] [TopologicalSpace X] [IsTopologicalGroup X]
    [ProCGroups.ProC.ProCGroup ProC X]
    [Group Y] [TopologicalSpace Y] [IsTopologicalGroup Y]
    [ProCGroups.ProC.ProCGroup ProC Y]
    [Group Z] [TopologicalSpace Z] [IsTopologicalGroup Z]
    [ProCGroups.ProC.ProCGroup ProC Z]
    (f : X →ₜ* Y) (g : Y →ₜ* Z) :
    ofHom (ProC := ProC) (g.comp f) = ofHom (ProC := ProC) f ≫ ofHom (ProC := ProC) g

\(\mathrm{ofHom}\) sends composition of continuous homomorphisms to categorical composition.

Show proof

Theorem ProCGrp.ofHom_apply GitHub

@[simp] theorem ofHom_apply {X Y : Type u}
    [Group X] [TopologicalSpace X] [IsTopologicalGroup X]
    [ProCGroups.ProC.ProCGroup ProC X]
    [Group Y] [TopologicalSpace Y] [IsTopologicalGroup Y]
    [ProCGroups.ProC.ProCGroup ProC Y]
    (f : X →ₜ* Y) (x : X) :
    ofHom (ProC := ProC) f x = f x

The bundled pro-\(C\) morphism \(\mathrm{ofHom}\) evaluates by applying the underlying continuous homomorphism.

Show proof

Instance ProCGrp.instHasForgetToProfiniteGrp GitHub

instance instHasForgetToProfiniteGrp : HasForget₂ (ProCGrp ProC) ProfiniteGrp where
  forget₂ :=
    { obj := fun G => G.toProfiniteGrp
      map := fun f => ProfiniteGrp.ofHom f.hom }

Forget a bundled pro-\(C\) group to its underlying profinite group.

Instance ProCGrp.instHasForgetToGrpCat GitHub

instance instHasForgetToGrpCat : HasForget₂ (ProCGrp ProC) GrpCat where
  forget₂ :=
    { obj := fun G => GrpCat.of G
      map := fun f => GrpCat.ofHom f.hom.toMonoidHom }

The forgetful functor to groups is available for pro-\(C\) groups.

Instance ProCGrp.instFaithfulForgetToProfiniteGrp GitHub

instance instFaithfulForgetToProfiniteGrp : (forget₂ (ProCGrp ProC) ProfiniteGrp).Faithful where
  map_injective := by
    intro X Y f g h
    ext x
    exact CategoryTheory.congr_fun h x

The forgetful functor from pro-\(C\) groups to profinite groups is faithful.

Instance ProCGrp.allFiniteProCGroup GitHub

instance allFiniteProCGroup (G : ProfiniteGrp.{u}) :
    ProCGroups.ProC.ProCGroup ProCGroups.ProC.allFiniteProC G :=
  ProCGroups.ProC.ProCGroup.of_isProCGroup ProCGroups.ProC.allFiniteProC G
    (ProCGroups.ProC.allFiniteProC_isProCGroup_of_profinite
      (ProCGroups.IsProfiniteGroup.of_profiniteGrp G))

Every underlying profinite group is a pro-\(C\) group for the all-finite predicate.

Definition ProCGrp.ofFiniteGrp GitHub

def ofFiniteGrp
    (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
    [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
    (G : FiniteGrp.{u}) (hG : ProC.finiteQuotientClass G) : ProCGrp ProC := by
  letI : TopologicalSpace G := ⊥
  letI : DiscreteTopology G := ⟨rfl⟩
  letI : IsTopologicalGroup G := inferInstance
  letI : ProCGroups.ProC.ProCGroup ProC G :=
    ProCGroups.ProC.ProCGroup.of_finite_discrete ProC hG
  exact of ProC G

A finite group in the finite quotient class \(C\), with the discrete topology, is a bundled pro-\(C\) group.

Definition ProCGrp.ofClosedSubgroup GitHub

def ofClosedSubgroup
    (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
    [ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
    [ProC.DeterminedByFiniteQuotients]
    (G : ProCGrp ProC) (H : ClosedSubgroup G) : ProCGrp ProC where
  toProfiniteGrp := ProfiniteGrp.ofClosedSubgroup (G := G.toProfiniteGrp) H
  proCGroup := by
    simpa using
      (ProCGroups.ProC.ProCGroup.of_closedSubgroup
        (G := G) ProC H)

Closed subgroups of pro-\(C\) groups are pro-\(C\).

Definition ProCGrp.ofContinuousMulEquiv GitHub

noncomputable def ofContinuousMulEquiv
    (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
    [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
    (G : ProCGrp ProC) {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (e : G ≃ₜ* H) : ProCGrp ProC := by
  letI : ProCGroups.ProC.ProCGroup ProC H :=
    ProCGroups.ProC.ProCGroup.ofContinuousMulEquiv (G := G) ProC e
  exact of ProC H

Transport a pro-\(C\) group structure across a continuous multiplicative equivalence.

Definition ProCGrp.pi GitHub

def pi
    (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
    [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
    {α : Type u} (β : α → ProCGrp ProC) : ProCGrp ProC := by
  let Pβ : α → ProfiniteGrp.{u} := fun a => (β a).toProfiniteGrp
  letI : ProCGroups.ProC.ProCGroup ProC ((a : α) → β a) :=
    ProCGroups.ProC.ProCGroup.pi (β := fun a => (β a : Type u)) ProC
  exact
    { toProfiniteGrp := ProfiniteGrp.pi Pβ
      proCGroup := by
        simpa [Pβ, ProfiniteGrp.pi] using
          (inferInstance : ProCGroups.ProC.ProCGroup ProC ((a : α) → β a)) }

Products of pro-\(C\) groups are pro-\(C\) when the finite quotient class is a formation.

Definition ProCGrp.quotientOpenNormalSubgroup GitHub

def quotientOpenNormalSubgroup
    (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
    [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
    (G : ProCGrp ProC) (U : OpenNormalSubgroup G) : ProCGrp ProC := by
  letI : ProCGroups.ProC.ProCGroup ProC (G ⧸ (U : Subgroup G)) :=
    ProCGroups.ProC.ProCGroup.quotient_openNormalSubgroup
      (G := G) ProC U
  exact of ProC (G ⧸ (U : Subgroup G))

Quotients by open normal subgroups of pro-\(C\) groups are pro-\(C\).

Definition ProCGrp.quotientOpenNormalSubgroupInClass GitHub

def quotientOpenNormalSubgroupInClass
    (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
    [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
    (G : ProCGrp ProC)
    (U : ProCGroups.ProC.OpenNormalSubgroupInClass ProC.finiteQuotientClass G) :
    ProCGrp ProC :=
  quotientOpenNormalSubgroup ProC G U.1

Quotients by open normal subgroups from the finite-quotient class family are pro-\(C\).

Definition ProCGrp.quotientClosedNormalSubgroup GitHub

def quotientClosedNormalSubgroup
    (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
    [ProC.HasFiniteQuotientMelnikovFormation] [ProC.DeterminedByFiniteQuotients]
    (G : ProCGrp ProC) (K : Subgroup G) [K.Normal] (hK : IsClosed (K : Set G)) :
    ProCGrp ProC := by
  letI : ProCGroups.ProC.ProCGroup ProC (G ⧸ K) :=
    ProCGroups.ProC.ProCGroup.quotient_closedNormalSubgroup
      (G := G) ProC K hK
  exact of ProC (G ⧸ K)

Quotients by closed normal subgroups of pro-\(C\) groups are pro-\(C\).

Definition ProCGrp.range GitHub

def range
    (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
    [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
    {A B : ProCGrp ProC} (f : A ⟶ B) : ProCGrp ProC := by
  letI : ProCGroups.ProC.ProCGroup ProC f.hom.toMonoidHom.range :=
    ProCGroups.ProC.ProCGroup.range
      (G := A) (H := B) ProC f.hom
  exact of ProC f.hom.toMonoidHom.range

The range of a morphism of pro-\(C\) groups, with its induced topology, is pro-\(C\).

Definition ProCGrp.kernel GitHub

def kernel
    (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
    [ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
    [ProC.DeterminedByFiniteQuotients]
    {A B : ProCGrp ProC} (f : A ⟶ B) : ProCGrp ProC := by
  let K : Subgroup A := f.hom.toMonoidHom.ker
  have hK : IsClosed (K : Set A) := by
    dsimp [K]
    exact f.hom.isClosed_ker
  letI : ProCGroups.ProC.ProCGroup ProC K :=
    ProCGroups.ProC.ProCGroup.of_isClosed_subgroup
      (G := A) ProC K hK
  exact of ProC K

The kernel subgroup of a morphism of pro-\(C\) groups, with its induced topology, is pro-\(C\).

ProCGroups.ProC.Category.Basic

Declarations