NYLL
Module

DenseFreeModel.lean

Nyll.ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.DenseFreeModel
15 declarations indexed from sourceView source ↗

Module documentation

Dense abstract free models of open subgroups

This module transports right-coset sections across a dense free-group lift, proves that the preimage of an open subgroup remains dense, and applies the discrete Nielsen--Schreier basis theorem to compute the abstract preimage rank. The result feeds the later pro-\(C\) completion argument.

Imports3
Imported by2

Declarations

theorem

rightRel_map_of_comap

L42 ↗
ReidemeisterSchreier.Profinite.rightRel_map_of_comap
Documentation

The right relator map is compatible with comap of the open subgroup.

Source context 13 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.WreathProducts
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u v w
section RightQuotientTransport
open _root_.ReidemeisterSchreier.FreeGroup
variable {F : Type u} [Group F]
variable {P : Type v} [Group P]
variable {Y : Type w}
Lean source · statement
theorem rightRel_map_of_comap
    (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
    (K : Subgroup P) (hβ : π.comp βF = β)
    {a b : FreeGroup Y}
    (hab : QuotientGroup.rightRel (Subgroup.comap β K) a b) :
    QuotientGroup.rightRel (Subgroup.comap π K) (βF a) (βF b)
def

mapRightQuotientOfComap

L56 ↗
ReidemeisterSchreier.Profinite.mapRightQuotientOfComap
Documentation

Transport right-coset classes along a homomorphism compatible with two subgroup preimages.

Source context 13 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.WreathProducts
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u v w
section RightQuotientTransport
open _root_.ReidemeisterSchreier.FreeGroup
variable {F : Type u} [Group F]
variable {P : Type v} [Group P]
variable {Y : Type w}
Lean source · full declaration
def mapRightQuotientOfComap :
    (π : F →* P) → (βF : FreeGroup Y →* F) → (β : FreeGroup Y →* P) →
      (K : Subgroup P) → (hβ : π.comp βF = β) →
    Quotient (QuotientGroup.rightRel (Subgroup.comap β K)) →
      Quotient (QuotientGroup.rightRel (Subgroup.comap π K))
  | π, βF, β, K, hβ =>
      Quotient.map' βF (fun _a _b hab => rightRel_map_of_comap π βF β K hβ hab)
theorem

surjective_mapRightQuotientOfComap

L66 ↗
ReidemeisterSchreier.Profinite.surjective_mapRightQuotientOfComap
Documentation

Surjectivity of the free-group map makes the induced map on right-quotient classes surjective.

Source context 13 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.WreathProducts
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u v w
section RightQuotientTransport
open _root_.ReidemeisterSchreier.FreeGroup
variable {F : Type u} [Group F]
variable {P : Type v} [Group P]
variable {Y : Type w}
Lean source · statement
theorem surjective_mapRightQuotientOfComap
    (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
    (K : Subgroup P) (hβ : π.comp βF = β)
    (hβsurj : Function.Surjective β) :
    Function.Surjective
      (mapRightQuotientOfComap π βF β K hβ)
theorem

injective_mapRightQuotientOfComap

L91 ↗
ReidemeisterSchreier.Profinite.injective_mapRightQuotientOfComap
Documentation

The induced map on right-quotient classes is injective under the comap compatibility equation.

Source context 13 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.WreathProducts
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u v w
section RightQuotientTransport
open _root_.ReidemeisterSchreier.FreeGroup
variable {F : Type u} [Group F]
variable {P : Type v} [Group P]
variable {Y : Type w}
Lean source · statement
theorem injective_mapRightQuotientOfComap
    (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
    (K : Subgroup P) (hβ : π.comp βF = β) :
    Function.Injective (mapRightQuotientOfComap π βF β K hβ)
def

rightQuotientEquivOfComap

L116 ↗
ReidemeisterSchreier.Profinite.rightQuotientEquivOfComap
Documentation

If \(\beta : \mathrm{FreeGroup}(Y) \to P\) is surjective and \(\beta = \pi \circ \beta_F\), then the right cosets of \(\beta^{-1}(K)\) are canonically identified with the right cosets of \(\pi^{-1}(K)\).

Source context 13 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.WreathProducts
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u v w
section RightQuotientTransport
open _root_.ReidemeisterSchreier.FreeGroup
variable {F : Type u} [Group F]
variable {P : Type v} [Group P]
variable {Y : Type w}
Lean source · statement
def rightQuotientEquivOfComap
    (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
    (K : Subgroup P) (hβ : π.comp βF = β)
    (hβsurj : Function.Surjective β) :
    Quotient (QuotientGroup.rightRel (Subgroup.comap β K)) ≃
      Quotient (QuotientGroup.rightRel (Subgroup.comap π K))
theorem

rightQuotientEquivOfComap_mk

L128 ↗
ReidemeisterSchreier.Profinite.rightQuotientEquivOfComap_mk
Documentation

The right-quotient comparison induced by comap is an equivalence.

Source context 13 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.WreathProducts
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u v w
section RightQuotientTransport
open _root_.ReidemeisterSchreier.FreeGroup
variable {F : Type u} [Group F]
variable {P : Type v} [Group P]
variable {Y : Type w}
Lean source · statement
theorem rightQuotientEquivOfComap_mk
    (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
    (K : Subgroup P) (hβ : π.comp βF = β)
    (hβsurj : Function.Surjective β) (w : FreeGroup Y) :
    rightQuotientEquivOfComap π βF β K hβ hβsurj
        (Quotient.mk'' w) =
      Quotient.mk'' (βF w)
def

rightSchreierSectionOfComap

L147 ↗
ReidemeisterSchreier.Profinite.rightSchreierSectionOfComap
Documentation

Transport a discrete Schreier transversal for \(\beta^{-1}(K)\) to a right-coset section for \(\pi^{-1}(K)\) in the ambient group \(F\).

Source context 16 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.WreathProducts
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u v w
section RightQuotientTransport
open _root_.ReidemeisterSchreier.FreeGroup
variable {F : Type u} [Group F]
variable {P : Type v} [Group P]
variable {Y : Type w}
section SchreierSections
variable [DecidableEq Y]
variable {T : Set (FreeGroup Y)}
Lean source · statement
def rightSchreierSectionOfComap
    (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
    (K : Subgroup P) (hβ : π.comp βF = β)
    (hβsurj : Function.Surjective β)
    (hT : IsRightSchreierTransversal (X := Y) (Subgroup.comap β K) T) :
    Quotient (QuotientGroup.rightRel (Subgroup.comap π K)) → F
theorem

rightSchreierSectionOfComap_spec

L159 ↗
ReidemeisterSchreier.Profinite.rightSchreierSectionOfComap_spec
Documentation

The transported right Schreier section satisfies its defining specification.

Source context 16 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.WreathProducts
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u v w
section RightQuotientTransport
open _root_.ReidemeisterSchreier.FreeGroup
variable {F : Type u} [Group F]
variable {P : Type v} [Group P]
variable {Y : Type w}
section SchreierSections
variable [DecidableEq Y]
variable {T : Set (FreeGroup Y)}
Lean source · statement
theorem rightSchreierSectionOfComap_spec
    (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
    (K : Subgroup P) (hβ : π.comp βF = β)
    (hβsurj : Function.Surjective β)
    (hT : IsRightSchreierTransversal (X := Y) (Subgroup.comap β K) T)
    (q : Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) :
    Quotient.mk'' (rightSchreierSectionOfComap π βF β K hβ hβsurj hT q) = q
theorem

rightSchreierSectionOfComap_eq_of_mem

L181 ↗
ReidemeisterSchreier.Profinite.rightSchreierSectionOfComap_eq_of_mem
Documentation

On a coset represented by an element of the chosen Schreier transversal, the transported section returns the image of that representative.

Source context 16 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.WreathProducts
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u v w
section RightQuotientTransport
open _root_.ReidemeisterSchreier.FreeGroup
variable {F : Type u} [Group F]
variable {P : Type v} [Group P]
variable {Y : Type w}
section SchreierSections
variable [DecidableEq Y]
variable {T : Set (FreeGroup Y)}
Lean source · statement
theorem rightSchreierSectionOfComap_eq_of_mem
    (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
    (K : Subgroup P) (hβ : π.comp βF = β)
    (hβsurj : Function.Surjective β)
    (hT : IsRightSchreierTransversal (X := Y) (Subgroup.comap β K) T)
    {t : FreeGroup Y} (ht : t ∈ T) :
    rightSchreierSectionOfComap π βF β K hβ hβsurj hT
        (Quotient.mk'' (βF t)) =
      βF t
theorem

rightSchreierSectionOfComap_one

L210 ↗
ReidemeisterSchreier.Profinite.rightSchreierSectionOfComap_one
Documentation

The transported Schreier section is normalized at the trivial right coset.

Source context 16 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.WreathProducts
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u v w
section RightQuotientTransport
open _root_.ReidemeisterSchreier.FreeGroup
variable {F : Type u} [Group F]
variable {P : Type v} [Group P]
variable {Y : Type w}
section SchreierSections
variable [DecidableEq Y]
variable {T : Set (FreeGroup Y)}
Lean source · statement
theorem rightSchreierSectionOfComap_one
    (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
    (K : Subgroup P) (hβ : π.comp βF = β)
    (hβsurj : Function.Surjective β)
    (hT : IsRightSchreierTransversal (X := Y) (Subgroup.comap β K) T) :
    rightSchreierSectionOfComap π βF β K hβ hβsurj hT
        (Quotient.mk'' (1 : F)) =
      1
theorem

denseRange_freeGroupLift_of_topologicallyGenerates

L235 ↗
ReidemeisterSchreier.Profinite.denseRange_freeGroupLift_of_topologicallyGenerates
Documentation

The abstract free-group lift of a topologically generating family has dense range.

Source context 13 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.WreathProducts
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u v w
section DenseAbstractFreeModel
open _root_.ReidemeisterSchreier.FreeGroup
variable {X : Type u}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {ι : X → F}
Lean source · statement
theorem denseRange_freeGroupLift_of_topologicallyGenerates
    (hgen : ProCGroups.Generation.TopologicallyGenerates (G := F) (Set.range ι)) :
    DenseRange (FreeGroup.lift ι : FreeGroup X →* F)
theorem

topologicallyGenerates_range_of_denseAbstractFreeLift

L255 ↗
ReidemeisterSchreier.Profinite.topologicallyGenerates_range_of_denseAbstractFreeLift
Documentation

A dense abstract free-group lift topologically generates through the images of the free generators.

Source context 13 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.WreathProducts
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u v w
section DenseAbstractFreeModel
open _root_.ReidemeisterSchreier.FreeGroup
variable {X : Type u}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {ι : X → F}
Lean source · full declaration
theorem topologicallyGenerates_range_of_denseAbstractFreeLift
    {Y : Type u}
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    {φ : FreeGroup Y →* H}
    (hφ : DenseRange φ) :
    ProCGroups.Generation.TopologicallyGenerates
      (G := H) (Set.range fun y : Y => φ (FreeGroup.of y)) := by
  let j : Y → H := fun y => φ (FreeGroup.of y)
  have himage :
      φ '' Set.range (FreeGroup.of : Y → FreeGroup Y) = Set.range j := by
    ext h
    constructor
    · rintro ⟨_, ⟨y, rfl⟩, rfl⟩
      exact ⟨y, rfl⟩
    · rintro ⟨y, rfl⟩
      exact ⟨FreeGroup.of y, ⟨y, rfl⟩, rfl⟩
  have hclosure :
      Subgroup.closure (Set.range j) = φ.range := by
    calc
      Subgroup.closure (Set.range j)
          = Subgroup.map φ (Subgroup.closure (Set.range (FreeGroup.of : Y → FreeGroup Y))) := by
              simpa [himage] using
                (φ.map_closure (Set.range (FreeGroup.of : Y → FreeGroup Y))).symm
      _ = φ.range := by
          rw [FreeGroup.closure_range_of Y, MonoidHom.range_eq_map]
  rw [ProCGroups.Generation.TopologicallyGenerates, hclosure]
  rw [SetLike.ext'_iff, Subgroup.topologicalClosure_coe, Subgroup.coe_top]
  simpa [DenseRange, MonoidHom.coe_range, dense_iff_closure_eq] using hφ
theorem

denseRange_comapMap_of_openSubgroup

L288 ↗
ReidemeisterSchreier.Profinite.denseRange_comapMap_of_openSubgroup
Documentation

Restricting a dense homomorphism to the preimage of an open subgroup still has dense range in that subgroup.

Source context 13 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.WreathProducts
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u v w
section DenseAbstractFreeModel
open _root_.ReidemeisterSchreier.FreeGroup
variable {X : Type u}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {ι : X → F}
Lean source · full declaration
theorem denseRange_comapMap_of_openSubgroup
    {G : Type u} [Group G]
    {H : Type u} [Group H] [TopologicalSpace H]
    {φ : G →* H} (hφ : DenseRange φ)
    {U : Subgroup H} (hU : IsOpen (U : Set H)) :
    DenseRange
      ({ toFun := fun g : Subgroup.comap φ U => ⟨φ g.1, g.2⟩
         map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
         map_mul' := by
           intro a b
           ext
           simp only [Subgroup.coe_mul, map_mul]} : Subgroup.comap φ U →* U) := by
  let ψ : Subgroup.comap φ U →* U :=
    { toFun := fun g => ⟨φ g.1, g.2⟩
      map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
      map_mul' := by
        intro a b
        ext
        simp only [Subgroup.coe_mul, map_mul]}
  have hdense : Dense (Set.range φ) := by
    simpa [DenseRange] using hφ
  have himage :
      ((↑) : U → H) '' Set.range ψ = (U : Set H) ∩ Set.range φ := by
    ext h
    constructor
    · rintro ⟨_, hu, rfl⟩
      rcases hu with ⟨g, rfl⟩
      exact ⟨g.2, ⟨g.1, rfl⟩⟩
    · rintro ⟨hu, g, rfl⟩
      exact ⟨⟨φ g, hu⟩, ⟨⟨g, hu⟩, rfl⟩, rfl⟩
  have hsubset :
      (U : Set H) ⊆ closure (((↑) : U → H) '' Set.range ψ) := by
    rw [himage]
    simpa [Set.inter_comm] using hdense.open_subset_closure_inter hU
  have hDenseU : Dense (Set.range ψ : Set U) := by
    exact (Subtype.dense_iff).2 hsubset
  change Dense (Set.range ψ)
  exact hDenseU
theorem

surjective_of_denseRange

L333 ↗
ReidemeisterSchreier.Profinite.surjective_of_denseRange
Documentation

A homomorphism into a finite discrete group is surjective as soon as it has dense range.

Source context 16 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.WreathProducts
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u v w
section DenseAbstractFreeModel
open _root_.ReidemeisterSchreier.FreeGroup
variable {X : Type u}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {ι : X → F}
section FiniteTargets
variable {P : Type u} [Group P] [TopologicalSpace P] [DiscreteTopology P] [Finite P]
omit [TopologicalSpace F] [IsTopologicalGroup F] [Finite P] in
Lean source · statement
theorem surjective_of_denseRange
    {φ : F →* P} (hφ : DenseRange φ) :
    Function.Surjective φ
theorem

exists_freeBasis_comap_freeGroupLift_of_openSubgroup_of_rankTransform

L352 ↗
ReidemeisterSchreier.Profinite.exists_freeBasis_comap_freeGroupLift_of_openSubgroup_of_rankTransform
Documentation

The abstract subgroup of \(\mathrm{FreeGroup}(X)\) lying over an open subgroup of a compact group via the dense free-group lift has the corresponding Schreier-transformed rank.

Source context 13 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.WreathProducts
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u v w
section DenseAbstractFreeModel
open _root_.ReidemeisterSchreier.FreeGroup
variable {X : Type u}
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {ι : X → F}
Lean source · statement
theorem exists_freeBasis_comap_freeGroupLift_of_openSubgroup_of_rankTransform
    {X : Type u} [Finite X]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F]
    {ι : X → F}
    (hgen : ProCGroups.Generation.TopologicallyGenerates (G := F) (Set.range ι))
    (H : OpenSubgroup F) :
    ∃ Y : Type u,
      Nonempty (FreeGroupBasis Y (Subgroup.comap (FreeGroup.lift ι) (H : Subgroup F))) ∧
      Nat.card Y = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F
          ⧸ (H : Subgroup F)))

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