Module

GeneratorDeletion.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorDeletion

46 declarations indexed from sourceView source ↗

Module documentation

Reidemeister Schreier / Discrete / Presentations / Tietze / Generator Deletion

This module formalizes deletion of generators forced to be trivial. It defines the elimination homomorphism and relator transformations and packages the induced equivalence of presented quotients.

Imports1

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorAddition

Imported by2

def

trivializeGeneratorsHom

L35 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.trivializeGeneratorsHom

Documentation

The substitution map sends the generators in \(Y\) to \(1\), while keeping the old generators \(X\). It is used by the Tietze move deleting generators with relators \(y = 1\).

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteTrivialGenerators
variable (X Y)

Lean source · statement

def trivializeGeneratorsHom : FreeGroup (Sum X Y) →* FreeGroup X

theorem

trivializeGeneratorsHom_inl

L42 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.trivializeGeneratorsHom_inl

Documentation

The trivializing homomorphism fixes each retained generator \(x : X\).

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteTrivialGenerators
variable (X Y)
variable {X Y}

Lean source · statement

theorem trivializeGeneratorsHom_inl (x : X) :
    trivializeGeneratorsHom X Y (FreeGroup.of (Sum.inl x)) =
      FreeGroup.of x

theorem

trivializeGeneratorsHom_inr

L49 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.trivializeGeneratorsHom_inr

Documentation

The trivializing homomorphism sends each deleted generator \(y : Y\) to \(1\).

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteTrivialGenerators
variable (X Y)
variable {X Y}

Lean source · statement

theorem trivializeGeneratorsHom_inr (y : Y) :
    trivializeGeneratorsHom X Y (FreeGroup.of (Sum.inr y)) = 1

theorem

trivializeGeneratorsHom_comp_include

L57 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.trivializeGeneratorsHom_comp_include

Documentation

Trivializing the deleted generators after including the retained generators is the identity on the retained free group.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteTrivialGenerators
variable (X Y)
variable {X Y}

Lean source · statement

theorem trivializeGeneratorsHom_comp_include :
    (trivializeGeneratorsHom X Y).comp (includeAdjoinedGenerators X Y) =
      MonoidHom.id (FreeGroup X)

def

trivialGeneratorRelators

L63 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.trivialGeneratorRelators

Documentation

Relators \(y = 1\) for a family of generators to be deleted.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteTrivialGenerators
variable (X Y)
variable {X Y}

Lean source · statement

def trivialGeneratorRelators :
    Set (FreeGroup (Sum X Y))

def

relatorsWithTrivialGenerators

L71 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.relatorsWithTrivialGenerators

Documentation

Adds the relators \(y = 1\) to a presentation over \(X \oplus Y\), trivializing the auxiliary generators.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteTrivialGenerators
variable (X Y)
variable {X Y}

Lean source · statement

def relatorsWithTrivialGenerators
    (R : Set (FreeGroup (Sum X Y))) :
    Set (FreeGroup (Sum X Y))

def

relatorsAfterDeletingTrivialGenerators

L79 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.relatorsAfterDeletingTrivialGenerators

Documentation

The relators after deleting the \(Y\)-generators are obtained by substituting them with \(1\).

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteTrivialGenerators
variable (X Y)
variable {X Y}

Lean source · statement

def relatorsAfterDeletingTrivialGenerators
    (R : Set (FreeGroup (Sum X Y))) :
    Set (FreeGroup X)

theorem

trivialGeneratorRelator_mem

L85 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.trivialGeneratorRelator_mem

Documentation

Each trivial-generator relation \(y = 1\) belongs to the trivial-generator relator set.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteTrivialGenerators
variable (X Y)
variable {X Y}

Lean source · statement

theorem trivialGeneratorRelator_mem (y : Y) :
    FreeGroup.of (Sum.inr y) ∈
      trivialGeneratorRelators (X := X) (Y := Y)

theorem

trivialGeneratorRelator_mem_relatorsWithTrivialGenerators

L91 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.trivialGeneratorRelator_mem_relatorsWithTrivialGenerators

Documentation

Each trivial-generator relation \(y = 1\) belongs to the relator set with trivial generators.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteTrivialGenerators
variable (X Y)
variable {X Y}

Lean source · statement

theorem trivialGeneratorRelator_mem_relatorsWithTrivialGenerators
    (R : Set (FreeGroup (Sum X Y))) (y : Y) :
    FreeGroup.of (Sum.inr y) ∈ relatorsWithTrivialGenerators R

theorem

relator_mem_relatorsWithTrivialGenerators

L97 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.relator_mem_relatorsWithTrivialGenerators

Documentation

Every original relator belongs to the relator set with trivial generators.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteTrivialGenerators
variable (X Y)
variable {X Y}

Lean source · statement

theorem relator_mem_relatorsWithTrivialGenerators
    {R : Set (FreeGroup (Sum X Y))} {r : FreeGroup (Sum X Y)}
    (hr : r ∈ R) :
    r ∈ relatorsWithTrivialGenerators R

theorem

include_trivializeGeneratorsHom_mod_trivialGeneratorRelators

L107 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.include_trivializeGeneratorsHom_mod_trivialGeneratorRelators

Documentation

Including the result of trivializing deleted generators is congruent to the original word modulo the trivial-generator relators.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteTrivialGenerators
variable (X Y)
variable {X Y}

Lean source · statement

theorem include_trivializeGeneratorsHom_mod_trivialGeneratorRelators
    (z : FreeGroup (Sum X Y)) :
    includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y z) * z⁻¹ ∈
      Subgroup.normalClosure (trivialGeneratorRelators (X := X) (Y := Y))

theorem

include_trivializeGeneratorsHom_mod_relatorsWithTrivialGenerators

L152 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.include_trivializeGeneratorsHom_mod_relatorsWithTrivialGenerators

Documentation

Including the result of trivializing deleted generators is congruent to the original word modulo the relators with trivial generators.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteTrivialGenerators
variable (X Y)
variable {X Y}

Lean source · statement

theorem include_trivializeGeneratorsHom_mod_relatorsWithTrivialGenerators
    (R : Set (FreeGroup (Sum X Y))) (z : FreeGroup (Sum X Y)) :
    includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y z) * z⁻¹ ∈
      Subgroup.normalClosure (relatorsWithTrivialGenerators R)

def

deleteTrivialGeneratorsMutualMapData

L165 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.deleteTrivialGeneratorsMutualMapData

Documentation

Deleting generators forced to be trivial gives mutual maps between the original presentation and the reduced presentation.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteTrivialGenerators
variable (X Y)
variable {X Y}

Lean source · full declaration

def deleteTrivialGeneratorsMutualMapData
    (R : Set (FreeGroup (Sum X Y))) :
    RelatorQuotientMutualMapData
      (relatorsWithTrivialGenerators R)
      (relatorsAfterDeletingTrivialGenerators R) where
  toHom := trivializeGeneratorsHom X Y
  invHom := includeAdjoinedGenerators X Y
  mapsRelators := by
    intro r hr
    rcases hr with hr | hr
    · exact Subgroup.subset_normalClosure ⟨r, hr, rfl⟩
    · rcases hr with ⟨y, rfl⟩
      simp only [trivializeGeneratorsHom_inr, one_mem]
  mapsTargetRelators := by
    intro s hs
    rcases hs with ⟨r, hr, rfl⟩
    let N : Subgroup (FreeGroup (Sum X Y)) :=
      Subgroup.normalClosure (relatorsWithTrivialGenerators R)
    have hmod :
        includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y r) *
            r⁻¹ ∈ N :=
      include_trivializeGeneratorsHom_mod_relatorsWithTrivialGenerators
        (X := X) (Y := Y) R r
    have hrN : r ∈ N :=
      Subgroup.subset_normalClosure
        (relator_mem_relatorsWithTrivialGenerators (R := R) hr)
    have hprod := Subgroup.mul_mem N hmod hrN
    convert hprod using 1
    group
  inv_toHom := by
    intro z
    exact include_trivializeGeneratorsHom_mod_relatorsWithTrivialGenerators
      (X := X) (Y := Y) R z
  to_invHom := by
    intro z
    have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f z)
      (trivializeGeneratorsHom_comp_include (X := X) (Y := Y))
    have hz :
        trivializeGeneratorsHom X Y (includeAdjoinedGenerators X Y z) = z := by
      simpa using hcomp
    simp only [hz, mul_inv_cancel, one_mem]

def

deleteTrivialGeneratorsTietzeEquiv

L208 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.deleteTrivialGeneratorsTietzeEquiv

Documentation

Tietze equivalence deleting generators forced to be trivial by the relators \(y = 1\).

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteTrivialGenerators
variable (X Y)
variable {X Y}

Lean source · statement

def deleteTrivialGeneratorsTietzeEquiv
    (R : Set (FreeGroup (Sum X Y))) :
    TietzeEquiv
      (relatorsWithTrivialGenerators R)
      (relatorsAfterDeletingTrivialGenerators R)

def

deleteTrivialGenerators

L220 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.deleteTrivialGenerators

Documentation

Tietze move deleting a family of generators that have relators y = 1. Every remaining relator is pushed forward by substituting those deleted generators with 1.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteTrivialGenerators
variable (X Y)
variable {X Y}

Lean source · statement

def deleteTrivialGenerators
    (R : Set (FreeGroup (Sum X Y))) :
    PresentedGroup (relatorsWithTrivialGenerators R) ≃*
      PresentedGroup (relatorsAfterDeletingTrivialGenerators R)

def

Kept

L235 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.GeneratorPartition.Kept

Documentation

Generators kept after deleting the generators satisfying delete.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}
namespace GeneratorPartition

Lean source · statement

def Kept (delete : Z → Prop) : Type _

def

Deleted

L239 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.GeneratorPartition.Deleted

Documentation

Generators deleted by a predicate delete.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}
namespace GeneratorPartition

Lean source · statement

def Deleted (delete : Z → Prop) : Type _

def

equiv

L245 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.GeneratorPartition.equiv

Documentation

Split an arbitrary generator type into the generators kept and deleted by a decidable predicate.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}
namespace GeneratorPartition

Lean source · full declaration

def equiv (delete : Z → Prop) [DecidablePred delete] :
    Z ≃ Sum (Kept delete) (Deleted delete) where
  toFun z :=
    if hz : delete z then
      Sum.inr ⟨z, hz⟩
    else
      Sum.inl ⟨z, hz⟩
  invFun z :=
    match z with
    | Sum.inl x => x.1
    | Sum.inr y => y.1
  left_inv z := by
    by_cases hz : delete z <;> simp only [hz, ↓reduceDIte]
  right_inv z := by
    cases z with
    | inl x =>
        simp only [Kept, Deleted, x.property, ↓reduceDIte]
        exact congrArg (fun z : Kept delete => (Sum.inl z : Sum (Kept delete) (Deleted delete)))
          (Subtype.ext rfl)
    | inr y =>
        simp only [Kept, Deleted, y.property, ↓reduceDIte]
        exact congrArg (fun z : Deleted delete => (Sum.inr z : Sum (Kept delete) (Deleted delete)))
          (Subtype.ext rfl)

theorem

equiv_apply_of_delete

L272 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.GeneratorPartition.equiv_apply_of_delete

Documentation

The partition equivalence sends a generator satisfying the deletion predicate to the deleted summand.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}
namespace GeneratorPartition

Lean source · statement

theorem equiv_apply_of_delete
    (delete : Z → Prop) [DecidablePred delete]
    {z : Z} (hz : delete z) :
    equiv delete z = Sum.inr (⟨z, hz⟩ : Deleted delete)

theorem

equiv_apply_of_not_delete

L281 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.GeneratorPartition.equiv_apply_of_not_delete

Documentation

The partition equivalence sends a retained generator to the kept summand.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}
namespace GeneratorPartition

Lean source · statement

theorem equiv_apply_of_not_delete
    (delete : Z → Prop) [DecidablePred delete]
    {z : Z} (hz : ¬ delete z) :
    equiv delete z = Sum.inl (⟨z, hz⟩ : Kept delete)

theorem

equiv_symm_inl

L290 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.GeneratorPartition.equiv_symm_inl

Documentation

The inverse partition equivalence forgets the proof attached to a retained generator.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}
namespace GeneratorPartition

Lean source · statement

theorem equiv_symm_inl
    (delete : Z → Prop) [DecidablePred delete]
    (z : Kept delete) :
    (equiv delete).symm (Sum.inl z) = z.1

theorem

equiv_symm_inr

L298 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.GeneratorPartition.equiv_symm_inr

Documentation

The inverse partition equivalence forgets the proof attached to a deleted generator.

Source context 8 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}
namespace GeneratorPartition

Lean source · statement

theorem equiv_symm_inr
    (delete : Z → Prop) [DecidablePred delete]
    (z : Deleted delete) :
    (equiv delete).symm (Sum.inr z) = z.1

def

definedGeneratorRelatorsAlongEquiv

L310 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.definedGeneratorRelatorsAlongEquiv

Documentation

Pull back the defining relators \(y = \mathrm{word}(y)\) along an equivalence that splits an arbitrary generator type into kept and deleted generators.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def definedGeneratorRelatorsAlongEquiv
    (e : Z ≃ Sum X Y) (word : Y → FreeGroup X) :
    Set (FreeGroup Z)

def

relatorsWithDefinedGeneratorsAlongEquiv

L320 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.relatorsWithDefinedGeneratorsAlongEquiv

Documentation

Add defining relators to an arbitrary presentation whose generator type is identified with \(X \oplus Y\).

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def relatorsWithDefinedGeneratorsAlongEquiv
    (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
    (word : Y → FreeGroup X) :
    Set (FreeGroup Z)

def

relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv

L330 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv

Documentation

Relators after renaming by \(e\) and substituting every deleted generator \(y : Y\) by \(\mathrm{word}(y)\).

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv
    (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
    (word : Y → FreeGroup X) :
    Set (FreeGroup X)

theorem

freeGroupCongr_image_definedGeneratorRelatorsAlongEquiv

L341 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.freeGroupCongr_image_definedGeneratorRelatorsAlongEquiv

Documentation

Renaming generators carries the pulled-back defining-generator relators to the defining-generator relators after the split.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

theorem freeGroupCongr_image_definedGeneratorRelatorsAlongEquiv
    (e : Z ≃ Sum X Y) (word : Y → FreeGroup X) :
    FreeGroup.freeGroupCongr e ''
        definedGeneratorRelatorsAlongEquiv e word =
      definedGeneratorRelators (X := X) (Y := Y) word

theorem

freeGroupCongr_image_relatorsWithDefinedGeneratorsAlongEquiv

L364 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.freeGroupCongr_image_relatorsWithDefinedGeneratorsAlongEquiv

Documentation

Renaming generators carries the pulled-back relators with defined generators to the corresponding split relator set.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

theorem freeGroupCongr_image_relatorsWithDefinedGeneratorsAlongEquiv
    (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
    (word : Y → FreeGroup X) :
    FreeGroup.freeGroupCongr e ''
        relatorsWithDefinedGeneratorsAlongEquiv R e word =
      relatorsWithDefinedGenerators
        (FreeGroup.freeGroupCongr e '' R) word

def

substituteDefinedGeneratorsAlongEquivTietzeEquiv

L396 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.substituteDefinedGeneratorsAlongEquivTietzeEquiv

Documentation

Tietze move eliminating an arbitrary family of generators after splitting the generator type by an equivalence \(Z \simeq X \oplus Y\).

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def substituteDefinedGeneratorsAlongEquivTietzeEquiv
    (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
    (word : Y → FreeGroup X) :
    TietzeEquiv
      (relatorsWithDefinedGeneratorsAlongEquiv R e word)
      (relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv R e word)

def

substituteDefinedGeneratorsAlongEquiv

L415 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.substituteDefinedGeneratorsAlongEquiv

Documentation

Defines substituteDefinedGeneratorsAlongEquiv.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def substituteDefinedGeneratorsAlongEquiv
    (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
    (word : Y → FreeGroup X) :
    PresentedGroup (relatorsWithDefinedGeneratorsAlongEquiv R e word) ≃*
      PresentedGroup
        (relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv R e word)

def

definedGeneratorRelatorsOfPredicate

L427 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.definedGeneratorRelatorsOfPredicate

Documentation

Add defining relations for all generators satisfying the deletion predicate; the kept generator type is the subtype of generators not satisfying that predicate.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def definedGeneratorRelatorsOfPredicate
    (delete : Z → Prop) [DecidablePred delete]
    (word :
      GeneratorPartition.Deleted delete →
        FreeGroup (GeneratorPartition.Kept delete)) :
    Set (FreeGroup Z)

def

relatorsWithDefinedGeneratorsOfPredicate

L440 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.relatorsWithDefinedGeneratorsOfPredicate

Documentation

The relator set obtained by adding defining relators for all generators satisfying the predicate.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def relatorsWithDefinedGeneratorsOfPredicate
    (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]
    (word :
      GeneratorPartition.Deleted delete →
        FreeGroup (GeneratorPartition.Kept delete)) :
    Set (FreeGroup Z)

def

relatorsAfterSubstitutingDefinedGeneratorsOfPredicate

L453 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.relatorsAfterSubstitutingDefinedGeneratorsOfPredicate

Documentation

Relators obtained after substituting every generator satisfying the predicate by its defining word.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def relatorsAfterSubstitutingDefinedGeneratorsOfPredicate
    (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]
    (word :
      GeneratorPartition.Deleted delete →
        FreeGroup (GeneratorPartition.Kept delete)) :
    Set (FreeGroup (GeneratorPartition.Kept delete))

def

substituteDefinedGeneratorsOfPredicateTietzeEquiv

L465 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.substituteDefinedGeneratorsOfPredicateTietzeEquiv

Documentation

Tietze equivalence substituting the generators satisfying the predicate by their defining words.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def substituteDefinedGeneratorsOfPredicateTietzeEquiv
    (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]
    (word :
      GeneratorPartition.Deleted delete →
        FreeGroup (GeneratorPartition.Kept delete)) :
    TietzeEquiv
      (relatorsWithDefinedGeneratorsOfPredicate R delete word)
      (relatorsAfterSubstitutingDefinedGeneratorsOfPredicate R delete word)

def

substituteDefinedGeneratorsOfPredicate

L477 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.substituteDefinedGeneratorsOfPredicate

Documentation

Defines substituteDefinedGeneratorsOfPredicate.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def substituteDefinedGeneratorsOfPredicate
    (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]
    (word :
      GeneratorPartition.Deleted delete →
        FreeGroup (GeneratorPartition.Kept delete)) :
    PresentedGroup (relatorsWithDefinedGeneratorsOfPredicate R delete word) ≃*
      PresentedGroup
        (relatorsAfterSubstitutingDefinedGeneratorsOfPredicate R delete word)

def

trivialGeneratorRelatorsAlongEquiv

L491 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.trivialGeneratorRelatorsAlongEquiv

Documentation

Pull back the trivial-generator relators \(y = 1\) along an equivalence that splits an arbitrary generator type into kept and deleted generators.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def trivialGeneratorRelatorsAlongEquiv
    (e : Z ≃ Sum X Y) :
    Set (FreeGroup Z)

def

relatorsWithTrivialGeneratorsAlongEquiv

L501 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.relatorsWithTrivialGeneratorsAlongEquiv

Documentation

Add trivial-generator relators to an arbitrary presentation whose generator type is identified with \(X \oplus Y\).

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def relatorsWithTrivialGeneratorsAlongEquiv
    (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
    Set (FreeGroup Z)

def

relatorsAfterDeletingTrivialGeneratorsAlongEquiv

L507 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.relatorsAfterDeletingTrivialGeneratorsAlongEquiv

Documentation

Relators after renaming by \(e\) and deleting every generator in \(Y\).

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def relatorsAfterDeletingTrivialGeneratorsAlongEquiv
    (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
    Set (FreeGroup X)

theorem

freeGroupCongr_image_trivialGeneratorRelatorsAlongEquiv

L516 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.freeGroupCongr_image_trivialGeneratorRelatorsAlongEquiv

Documentation

Renaming generators carries the pulled-back trivial-generator relators to the trivial-generator relators after the split.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

theorem freeGroupCongr_image_trivialGeneratorRelatorsAlongEquiv
    (e : Z ≃ Sum X Y) :
    FreeGroup.freeGroupCongr e ''
        trivialGeneratorRelatorsAlongEquiv (X := X) (Y := Y) e =
      trivialGeneratorRelators (X := X) (Y := Y)

theorem

freeGroupCongr_image_relatorsWithTrivialGeneratorsAlongEquiv

L539 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.freeGroupCongr_image_relatorsWithTrivialGeneratorsAlongEquiv

Documentation

Renaming generators carries the pulled-back relators with trivial generators to the corresponding split relator set.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

theorem freeGroupCongr_image_relatorsWithTrivialGeneratorsAlongEquiv
    (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
    FreeGroup.freeGroupCongr e ''
        relatorsWithTrivialGeneratorsAlongEquiv R e =
      relatorsWithTrivialGenerators (FreeGroup.freeGroupCongr e '' R)

def

deleteTrivialGeneratorsAlongEquivTietzeEquiv

L569 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.deleteTrivialGeneratorsAlongEquivTietzeEquiv

Documentation

Tietze move deleting an arbitrary family of generators after splitting the generator type by an equivalence \(Z \simeq X \oplus Y\).

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def deleteTrivialGeneratorsAlongEquivTietzeEquiv
    (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
    TietzeEquiv
      (relatorsWithTrivialGeneratorsAlongEquiv R e)
      (relatorsAfterDeletingTrivialGeneratorsAlongEquiv R e)

def

deleteTrivialGeneratorsAlongEquiv

L587 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.deleteTrivialGeneratorsAlongEquiv

Documentation

Defines deleteTrivialGeneratorsAlongEquiv.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def deleteTrivialGeneratorsAlongEquiv
    (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
    PresentedGroup (relatorsWithTrivialGeneratorsAlongEquiv R e) ≃*
      PresentedGroup
        (relatorsAfterDeletingTrivialGeneratorsAlongEquiv R e)

def

trivialGeneratorRelatorsOfPredicate

L595 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.trivialGeneratorRelatorsOfPredicate

Documentation

Trivial-generator relators for the generators satisfying the deletion predicate.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def trivialGeneratorRelatorsOfPredicate
    (delete : Z → Prop) [DecidablePred delete] :
    Set (FreeGroup Z)

def

relatorsWithTrivialGeneratorsOfPredicate

L607 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.relatorsWithTrivialGeneratorsOfPredicate

Documentation

The relator set obtained by adding trivial-generator relators for all generators satisfying the predicate.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def relatorsWithTrivialGeneratorsOfPredicate
    (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :
    Set (FreeGroup Z)

def

relatorsAfterDeletingTrivialGeneratorsOfPredicate

L619 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.relatorsAfterDeletingTrivialGeneratorsOfPredicate

Documentation

Relators obtained after deleting every generator satisfying the predicate by substituting it with \(1\).

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def relatorsAfterDeletingTrivialGeneratorsOfPredicate
    (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :
    Set (FreeGroup (GeneratorPartition.Kept delete))

def

deleteTrivialGeneratorsOfPredicateTietzeEquiv

L628 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.deleteTrivialGeneratorsOfPredicateTietzeEquiv

Documentation

Tietze equivalence deleting the generators satisfying the chosen predicate.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def deleteTrivialGeneratorsOfPredicateTietzeEquiv
    (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :
    TietzeEquiv
      (relatorsWithTrivialGeneratorsOfPredicate R delete)
      (relatorsAfterDeletingTrivialGeneratorsOfPredicate R delete)

def

deleteTrivialGeneratorsOfPredicate

L639 ↗

ReidemeisterSchreier.Discrete.Presentations.Presented.deleteTrivialGeneratorsOfPredicate

Documentation

Defines deleteTrivialGeneratorsOfPredicate.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
namespace Presented
variable {X Y : Type*}
section AdjoinGenerators
section DeleteGeneratorsAlongEquiv
variable {Z X Y : Type*}

Lean source · statement

def deleteTrivialGeneratorsOfPredicate
    (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :
    PresentedGroup (relatorsWithTrivialGeneratorsOfPredicate R delete) ≃*
      PresentedGroup
        (relatorsAfterDeletingTrivialGeneratorsOfPredicate R delete)

Module documentation

Reidemeister Schreier / Discrete / Presentations / Tietze / Generator Deletion

Declarations