Module

InjectiveRestriction.lean

Nyll.EtaleFundamentalGroups.ContinuousActions.InjectiveRestriction

4 declarations indexed from sourceView source ↗

Module documentation

Injectivity detected by finite continuous actions

A continuous homomorphism of profinite groups is injective exactly when every nonempty transitive finite continuous action of the source has the epi--mono span of Stacks Project, Tag 0BN7.

Imports8

Nyll.ProCGroups.ProC.Quotients.ClosedSubgroupNeighborhoods
Nyll.ProCGroups.ProC.Quotients.LeftQuotientProjectionSections
Nyll.EtaleFundamentalGroups.ContinuousActions.FiniteLimitsAndColimits
Mathlib.CategoryTheory.Action.Concrete
Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Mathlib.GroupTheory.GroupAction.Transitive
Mathlib.GroupTheory.GroupAction.Quotient
Mathlib.Topology.Algebra.ClopenNhdofOne

Imported by2

theorem

exists_openNormalSubgroup_comap_le

L34 ↗

CategoryTheory.ContAction.exists_openNormalSubgroup_comap_le

Source context 5 commands

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

noncomputable section
universe g' g w
open CategoryTheory
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction

Lean source · statement

theorem exists_openNormalSubgroup_comap_le
    {G' : Type g'} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G']
      [CompactSpace G']
    {G : Type g} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
      [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (h : G' →ₜ* G) (hinj : Function.Injective h)
    (U : OpenSubgroup G') :
    ∃ V : OpenNormalSubgroup G,
      (V : Subgroup G).comap h.toMonoidHom ≤ (U : Subgroup G')

theorem

exists_epi_mono_span_of_injective

L86 ↗

CategoryTheory.ContAction.exists_epi_mono_span_of_injective

Source context 8 commands

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

noncomputable section
universe g' g w
open CategoryTheory
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G' : Type g'} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G']
  [CompactSpace G'] [TotallyDisconnectedSpace G']
variable {G : Type g} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [TotallyDisconnectedSpace G'] in

Lean source · statement

theorem exists_epi_mono_span_of_injective
    (h : G' →ₜ* G) (hinj : Function.Injective h)
    (X' : ContAction FintypeCat.{w} G')
    (hnon : Nonempty X'.obj.V)
    (htrans : MulAction.IsPretransitive G' X'.obj.V) :
    ∃ (X : ContAction FintypeCat.{w} G)
      (Y : ContAction FintypeCat.{w} G')
      (q : Y ⟶ X')
      (i : Y ⟶ (ContAction.res FintypeCat h).obj X),
      Epi q ∧ Mono i

theorem

injective_of_exists_epi_mono_span

L208 ↗

CategoryTheory.ContAction.injective_of_exists_epi_mono_span

Source context 8 commands

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

noncomputable section
universe g' g w
open CategoryTheory
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G' : Type g'} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G']
  [CompactSpace G'] [TotallyDisconnectedSpace G']
variable {G : Type g} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
  [TotallyDisconnectedSpace G] in

Lean source · statement

theorem injective_of_exists_epi_mono_span
    (h : G' →ₜ* G)
    (hspan :
      ∀ X' : ContAction FintypeCat.{w} G',
        Nonempty X'.obj.V →
        MulAction.IsPretransitive G' X'.obj.V →
        ∃ (X : ContAction FintypeCat.{w} G)
          (Y : ContAction FintypeCat.{w} G')
          (q : Y ⟶ X')
          (i : Y ⟶ (ContAction.res FintypeCat h).obj X),
          Epi q ∧ Mono i) :
    Function.Injective h

theorem

injective_iff_exists_epi_mono_span

L327 ↗

CategoryTheory.ContAction.injective_iff_exists_epi_mono_span

Documentation

A continuous homomorphism of profinite groups is injective exactly when every nonempty transitive finite continuous source action has an epimorphism from a finite continuous source action that embeds in a restricted target action.

Source context 7 commands

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

noncomputable section
universe g' g w
open CategoryTheory
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G' : Type g'} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G']
  [CompactSpace G'] [TotallyDisconnectedSpace G']
variable {G : Type g} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · statement

theorem injective_iff_exists_epi_mono_span
    (h : G' →ₜ* G) :
    Function.Injective h ↔
      ∀ X' : ContAction FintypeCat.{w} G',
        Nonempty X'.obj.V →
        MulAction.IsPretransitive G' X'.obj.V →
        ∃ (X : ContAction FintypeCat.{w} G)
          (Y : ContAction FintypeCat.{w} G')
          (q : Y ⟶ X')
          (i : Y ⟶ (ContAction.res FintypeCat h).obj X),
          Epi q ∧ Mono i

Module documentation

Injectivity detected by finite continuous actions

Declarations

exists_openNormalSubgroup_comap_le

exists_epi_mono_span_of_injective

injective_of_exists_epi_mono_span

injective_iff_exists_epi_mono_span