ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorMap

1 Theorem | 8 Definition

This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.

Open this file on GitHub

import

ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorQuotientMutualMapData

Imported by

Definition ReidemeisterSchreier.Discrete.Presentations.relatorQuotientMutualMapDataOfRelatorImagesMemNormalClosure GitHub

def relatorQuotientMutualMapDataOfRelatorImagesMemNormalClosure
    (e : G ≃* H) (R : Set G) (S : Set H)
    (hR_to_S : ∀ r ∈ R, e r ∈ Subgroup.normalClosure S)
    (hS_to_R : ∀ s ∈ S, e.symm s ∈ Subgroup.normalClosure R) :
    RelatorQuotientMutualMapData R S :=
  relatorQuotientMutualMapDataOfNormalClosureMapEq R S e
    (map_normalClosure_eq_of_mulEquiv_relator_images_mem_normalClosure e R S hR_to_S hS_to_R)

The relator membership follows from the corresponding relator-equivalence criterion.

Definition ReidemeisterSchreier.Discrete.Presentations.relatorQuotientMutualMapDataOfGeneratorMaps GitHub

def relatorQuotientMutualMapDataOfGeneratorMaps
    {X Y : Type*} {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
    (toGenerator : X → FreeGroup Y)
    (invGenerator : Y → FreeGroup X)
    (hR :
      ∀ r ∈ R,
        FreeGroup.lift toGenerator r ∈ Subgroup.normalClosure S)
    (hS :
      ∀ s ∈ S,
        FreeGroup.lift invGenerator s ∈ Subgroup.normalClosure R)
    (hinv_to :
      ∀ x : X,
        RelatorEquivalent R
          (FreeGroup.lift invGenerator (toGenerator x))
          (FreeGroup.of x))
    (hto_inv :
      ∀ y : Y,
        RelatorEquivalent S
          (FreeGroup.lift toGenerator (invGenerator y))
          (FreeGroup.of y)) :
    RelatorQuotientMutualMapData R S where
  toHom := FreeGroup.lift toGenerator
  invHom := FreeGroup.lift invGenerator
  mapsRelators := hR
  mapsTargetRelators := hS
  inv_toHom := by
    intro w
    let N : Subgroup (FreeGroup X) := Subgroup.normalClosure R
    let F : FreeGroup X →* FreeGroup X ⧸ N :=
      (QuotientGroup.mk' N).comp
        ((FreeGroup.lift invGenerator).comp (FreeGroup.lift toGenerator))
    have hhom : F = QuotientGroup.mk' N := by
      ext x
      dsimp [F]
      simp only [FreeGroup.lift_apply_of]
      rw [← relatorEquivalent_iff_eq_in_presentedQuotient]
      exact hinv_to x
    have hw := congrArg (fun f : FreeGroup X →* FreeGroup X ⧸ N => f w) hhom
    change
      ((FreeGroup.lift invGenerator
          (FreeGroup.lift toGenerator w) : FreeGroup X) :
        FreeGroup X ⧸ N) =
      ((w : FreeGroup X) : FreeGroup X ⧸ N) at hw
    exact (by
      simpa [N, RelatorEquivalent] using
        (relatorEquivalent_iff_eq_in_presentedQuotient.2 hw :
          RelatorEquivalent R
            (FreeGroup.lift invGenerator (FreeGroup.lift toGenerator w)) w))
  to_invHom := by
    intro w
    let N : Subgroup (FreeGroup Y) := Subgroup.normalClosure S
    let F : FreeGroup Y →* FreeGroup Y ⧸ N :=
      (QuotientGroup.mk' N).comp
        ((FreeGroup.lift toGenerator).comp (FreeGroup.lift invGenerator))
    have hhom : F = QuotientGroup.mk' N := by
      ext y
      dsimp [F]
      simp only [FreeGroup.lift_apply_of]
      rw [← relatorEquivalent_iff_eq_in_presentedQuotient]
      exact hto_inv y
    have hw := congrArg (fun f : FreeGroup Y →* FreeGroup Y ⧸ N => f w) hhom
    change
      ((FreeGroup.lift toGenerator
          (FreeGroup.lift invGenerator w) : FreeGroup Y) :
        FreeGroup Y ⧸ N) =
      ((w : FreeGroup Y) : FreeGroup Y ⧸ N) at hw
    exact (by
      simpa [N, RelatorEquivalent] using
        (relatorEquivalent_iff_eq_in_presentedQuotient.2 hw :
          RelatorEquivalent S
            (FreeGroup.lift toGenerator (FreeGroup.lift invGenerator w)) w))

Compatible generator maps in both directions define mutual map data on the corresponding relator quotients.

Definition ReidemeisterSchreier.Discrete.Presentations.relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent GitHub

def relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent
    {X Y : Type*} {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
    (toGenerator : X → FreeGroup Y)
    (invGenerator : Y → FreeGroup X)
    (hR :
      ∀ r ∈ R,
        RelatorEquivalent S (FreeGroup.lift toGenerator r) 1)
    (hS :
      ∀ s ∈ S,
        RelatorEquivalent R (FreeGroup.lift invGenerator s) 1)
    (hinv_to :
      ∀ x : X,
        RelatorEquivalent R
          (FreeGroup.lift invGenerator (toGenerator x))
          (FreeGroup.of x))
    (hto_inv :
      ∀ y : Y,
        RelatorEquivalent S
          (FreeGroup.lift toGenerator (invGenerator y))
          (FreeGroup.of y)) :
    RelatorQuotientMutualMapData R S :=
  relatorQuotientMutualMapDataOfGeneratorMaps
    toGenerator invGenerator
    (fun r hr => RelatorEquivalent.mem_normalClosure_of_eq_one (hR r hr))
    (fun s hs => RelatorEquivalent.mem_normalClosure_of_eq_one (hS s hs))
    hinv_to hto_inv

Generator maps that preserve relators up to relator equivalence give mutual map data between relator quotients.

Definition ReidemeisterSchreier.Discrete.Presentations.relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent_iUnion GitHub

def relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent_iUnion
    {X Y : Type*} {ι κ : Sort*}
    {R : ι → Set (FreeGroup X)} {S : κ → Set (FreeGroup Y)}
    (toGenerator : X → FreeGroup Y)
    (invGenerator : Y → FreeGroup X)
    (hR :
      ∀ i : ι, ∀ r ∈ R i,
        RelatorEquivalent (Set.iUnion S) (FreeGroup.lift toGenerator r) 1)
    (hS :
      ∀ k : κ, ∀ s ∈ S k,
        RelatorEquivalent (Set.iUnion R) (FreeGroup.lift invGenerator s) 1)
    (hinv_to :
      ∀ x : X,
        RelatorEquivalent (Set.iUnion R)
          (FreeGroup.lift invGenerator (toGenerator x))
          (FreeGroup.of x))
    (hto_inv :
      ∀ y : Y,
        RelatorEquivalent (Set.iUnion S)
          (FreeGroup.lift toGenerator (invGenerator y))
          (FreeGroup.of y)) :
    RelatorQuotientMutualMapData (Set.iUnion R) (Set.iUnion S) :=
  relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent
    toGenerator invGenerator
    (by
      intro r hr
      rcases Set.mem_iUnion.1 hr with ⟨i, hi⟩
      exact hR i r hi)
    (by
      intro s hs
      rcases Set.mem_iUnion.1 hs with ⟨k, hk⟩
      exact hS k s hk)
    hinv_to hto_inv

Generator-map certificate for presentations whose relators are indexed families. This is an application-facing dispatcher: a downstream proof can check source and target relators one family at a time.

Definition ReidemeisterSchreier.Discrete.Presentations.relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent_iUnion₂ GitHub

def relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent_iUnion₂
    {X Y : Type*} {ι κ : Sort*} {α : ι → Sort*} {β : κ → Sort*}
    {R : ∀ i : ι, α i → Set (FreeGroup X)}
    {S : ∀ k : κ, β k → Set (FreeGroup Y)}
    (toGenerator : X → FreeGroup Y)
    (invGenerator : Y → FreeGroup X)
    (hR :
      ∀ i : ι, ∀ a : α i, ∀ r ∈ R i a,
        RelatorEquivalent
          (Set.iUnion fun k : κ => Set.iUnion (S k))
          (FreeGroup.lift toGenerator r) 1)
    (hS :
      ∀ k : κ, ∀ b : β k, ∀ s ∈ S k b,
        RelatorEquivalent
          (Set.iUnion fun i : ι => Set.iUnion (R i))
          (FreeGroup.lift invGenerator s) 1)
    (hinv_to :
      ∀ x : X,
        RelatorEquivalent
          (Set.iUnion fun i : ι => Set.iUnion (R i))
          (FreeGroup.lift invGenerator (toGenerator x))
          (FreeGroup.of x))
    (hto_inv :
      ∀ y : Y,
        RelatorEquivalent
          (Set.iUnion fun k : κ => Set.iUnion (S k))
          (FreeGroup.lift toGenerator (invGenerator y))
          (FreeGroup.of y)) :
    RelatorQuotientMutualMapData
      (Set.iUnion fun i : ι => Set.iUnion (R i))
      (Set.iUnion fun k : κ => Set.iUnion (S k)) :=
  relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent
    toGenerator invGenerator
    (by
      intro r hr
      rcases Set.mem_iUnion.1 hr with ⟨i, hi⟩
      rcases Set.mem_iUnion.1 hi with ⟨a, ha⟩
      exact hR i a r ha)
    (by
      intro s hs
      rcases Set.mem_iUnion.1 hs with ⟨k, hk⟩
      rcases Set.mem_iUnion.1 hk with ⟨b, hb⟩
      exact hS k b s hb)
    hinv_to hto_inv

Generator maps that preserve doubly indexed relator families give mutual map data between the relator quotients.

Definition ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorSet GitHub

def freeGroupPullbackRelatorSet
    {Y : Type*} (e : FreeGroup Y ≃* G) (S : Set G) :
    Set (FreeGroup Y) :=
  e.symm '' S

Two-level family variant of relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent_iUnion.

Theorem ReidemeisterSchreier.Discrete.Presentations.map_normalClosure_freeGroupPullbackRelatorSet GitHub

theorem map_normalClosure_freeGroupPullbackRelatorSet
    {Y : Type*} (e : FreeGroup Y ≃* G) (S : Set G) :
    Subgroup.map e.toMonoidHom
        (Subgroup.normalClosure (freeGroupPullbackRelatorSet e S)) =
      Subgroup.normalClosure S

The free-kernel relators map into the corresponding normal closure.

Show proof

Definition ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorQuotientEquiv GitHub

noncomputable def freeGroupPullbackRelatorQuotientEquiv
    {Y : Type*} (e : FreeGroup Y ≃* G) (S : Set G) :
    FreeGroup Y ⧸
        Subgroup.normalClosure (freeGroupPullbackRelatorSet e S) ≃*
      G ⧸ Subgroup.normalClosure S :=
  QuotientGroup.congr
    (Subgroup.normalClosure (freeGroupPullbackRelatorSet e S))
    (Subgroup.normalClosure S)
    e
    (map_normalClosure_freeGroupPullbackRelatorSet e S)

A free-group equivalence identifies the quotient by a relator set with the quotient by its pullback relator set.

Definition ReidemeisterSchreier.Discrete.Presentations.quotientEquivOfRelatorQuotientMutualMapData GitHub

noncomputable def quotientEquivOfRelatorQuotientMutualMapData
    (R : Set G) (S : Set H)
    (hData : RelatorQuotientMutualMapData R S) :
    G ⧸ Subgroup.normalClosure R ≃* H ⧸ Subgroup.normalClosure S :=
  quotientEquivOfRelatorsByMutualMaps R S
    hData.toHom hData.invHom hData.mapsRelators hData.mapsTargetRelators
    hData.inv_toHom hData.to_invHom

Mutual relator-quotient map data induce an isomorphism of the corresponding quotients.

ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorMap

Declarations