NYLL
Module

Core.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.Core
25 declarations indexed from sourceView source ↗

Module documentation

Semantic equivalence of presentations

This module packages the algebraic content of a Tietze equivalence: mutually inverse maps between groups presented by relators. Presentation remembers the generator type, while PresentationEquivCertificate composes and reverses the resulting semantic certificates.

Concrete, inspectable move sequences are defined separately in Tietze.Script.

Imports2
Imported by2

Declarations

structure

TietzeEquiv

L29 ↗
ReidemeisterSchreier.Discrete.Presentations.TietzeEquiv
Documentation

A reusable semantic Tietze certificate between two relator presentations.

Source context 3 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
Lean source · full declaration
structure TietzeEquiv
    {X Y : Type*} (R : Set (FreeGroup X)) (S : Set (FreeGroup Y)) where
  /-- Mutually inverse maps between the two free groups, modulo their relator normal closures. -/
  toMutualMapData : RelatorQuotientMutualMapData R S
def

refl

L41 ↗
ReidemeisterSchreier.Discrete.Presentations.TietzeEquiv.refl
Documentation

The identity mutual map gives a reflexive Tietze equivalence.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace TietzeEquiv
variable {X Y Z : Type*}
variable {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
variable {T : Set (FreeGroup Z)}
Lean source · full declaration
def refl (R : Set (FreeGroup X)) : TietzeEquiv R R where
  toMutualMapData := RelatorQuotientMutualMapData.refl R
def

symm

L45 ↗
ReidemeisterSchreier.Discrete.Presentations.TietzeEquiv.symm
Documentation

Reversing the mutual maps gives the symmetric Tietze equivalence.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace TietzeEquiv
variable {X Y Z : Type*}
variable {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
variable {T : Set (FreeGroup Z)}
Lean source · full declaration
def symm (D : TietzeEquiv R S) : TietzeEquiv S R where
  toMutualMapData := D.toMutualMapData.symm
def

trans

L49 ↗
ReidemeisterSchreier.Discrete.Presentations.TietzeEquiv.trans
Documentation

Composing mutual maps gives the transitive composite of Tietze equivalences.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace TietzeEquiv
variable {X Y Z : Type*}
variable {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
variable {T : Set (FreeGroup Z)}
Lean source · full declaration
def trans (D₁ : TietzeEquiv R S) (D₂ : TietzeEquiv S T) :
    TietzeEquiv R T where
  toMutualMapData := D₁.toMutualMapData.trans D₂.toMutualMapData
def

ofMutualMapData

L54 ↗
ReidemeisterSchreier.Discrete.Presentations.TietzeEquiv.ofMutualMapData
Documentation

Mutual relator-quotient map data define a Tietze equivalence.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace TietzeEquiv
variable {X Y Z : Type*}
variable {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
variable {T : Set (FreeGroup Z)}
Lean source · full declaration
def ofMutualMapData (D : RelatorQuotientMutualMapData R S) :
    TietzeEquiv R S where
  toMutualMapData := D
def

ofRelatorEquivalent

L62 ↗
ReidemeisterSchreier.Discrete.Presentations.TietzeEquiv.ofRelatorEquivalent
Documentation

A Tietze equivalence is induced by a relator-equivalence comparison between the two relator sets.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace TietzeEquiv
variable {X Y Z : Type*}
variable {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
variable {T : Set (FreeGroup Z)}
Lean source · full declaration
def ofRelatorEquivalent
    {R S : Set (FreeGroup X)}
    (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
    (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
    TietzeEquiv R S where
  toMutualMapData :=
    relatorQuotientMutualMapDataOfRelatorEquivalent hR_to_S hS_to_R
def

ofNormalClosureEq

L71 ↗
ReidemeisterSchreier.Discrete.Presentations.TietzeEquiv.ofNormalClosureEq
Documentation

Equal normal closures give a Tietze equivalence between the two relator sets.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace TietzeEquiv
variable {X Y Z : Type*}
variable {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
variable {T : Set (FreeGroup Z)}
Lean source · full declaration
def ofNormalClosureEq
    {R S : Set (FreeGroup X)}
    (h : Subgroup.normalClosure R = Subgroup.normalClosure S) :
    TietzeEquiv R S where
  toMutualMapData := relatorQuotientMutualMapDataOfNormalClosureEq h
def

ofGeneratorMaps

L81 ↗
ReidemeisterSchreier.Discrete.Presentations.TietzeEquiv.ofGeneratorMaps
Documentation

Compatible generator maps in both directions define a Tietze equivalence between the two relator quotients.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace TietzeEquiv
variable {X Y Z : Type*}
variable {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
variable {T : Set (FreeGroup Z)}
Lean source · statement
def ofGeneratorMaps
    {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)) :
    TietzeEquiv R S
def

ofGeneratorMapsRelatorEquivalent

L110 ↗
ReidemeisterSchreier.Discrete.Presentations.TietzeEquiv.ofGeneratorMapsRelatorEquivalent
Documentation

Generator maps that preserve relators up to relator equivalence induce the corresponding presented-group map.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace TietzeEquiv
variable {X Y Z : Type*}
variable {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
variable {T : Set (FreeGroup Z)}
Lean source · statement
def ofGeneratorMapsRelatorEquivalent
    {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)) :
    TietzeEquiv R S
def

ofGeneratorMapsRelatorEquivalent_iUnion

L139 ↗
ReidemeisterSchreier.Discrete.Presentations.TietzeEquiv.ofGeneratorMapsRelatorEquivalent_iUnion
Documentation

A Tietze certificate from generator maps when both relator sets are indexed unions of named relator families.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace TietzeEquiv
variable {X Y Z : Type*}
variable {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
variable {T : Set (FreeGroup Z)}
Lean source · statement
def ofGeneratorMapsRelatorEquivalent_iUnion
    {ι κ : 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)) :
    TietzeEquiv (Set.iUnion R) (Set.iUnion S)
def

ofGeneratorMapsRelatorEquivalent_iUnion₂

L169 ↗
ReidemeisterSchreier.Discrete.Presentations.TietzeEquiv.ofGeneratorMapsRelatorEquivalent_iUnion₂
Documentation

A Tietze equivalence is obtained from generator maps whose doubly indexed source relators map to relator-equivalent target relators.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace TietzeEquiv
variable {X Y Z : Type*}
variable {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
variable {T : Set (FreeGroup Z)}
Lean source · full declaration
def ofGeneratorMapsRelatorEquivalent_iUnion₂
    {ι κ : 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)) :
    TietzeEquiv
      (Set.iUnion fun i : ι => Set.iUnion (R i))
      (Set.iUnion fun k : κ => Set.iUnion (S k)) :=
  TietzeEquiv.ofMutualMapData
    (relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent_iUnion₂
      toGenerator invGenerator hR hS hinv_to hto_inv)
def

quotientEquiv

L205 ↗
ReidemeisterSchreier.Discrete.Presentations.TietzeEquiv.quotientEquiv
Documentation

A Tietze equivalence induces an isomorphism of the corresponding relator quotients.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace TietzeEquiv
variable {X Y Z : Type*}
variable {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
variable {T : Set (FreeGroup Z)}
Lean source · statement
def quotientEquiv (D : TietzeEquiv R S) :
    FreeGroup X ⧸ Subgroup.normalClosure R ≃*
      FreeGroup Y ⧸ Subgroup.normalClosure S
def

presentedEquiv

L211 ↗
ReidemeisterSchreier.Discrete.Presentations.TietzeEquiv.presentedEquiv
Documentation

A Tietze equivalence induces an isomorphism of presented groups.

Source context 7 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace TietzeEquiv
variable {X Y Z : Type*}
variable {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
variable {T : Set (FreeGroup Z)}
Lean source · statement
def presentedEquiv (D : TietzeEquiv R S) :
    PresentedGroup R ≃* PresentedGroup S
def

freeGroupPullbackRelatorTietzeEquiv

L221 ↗
ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorTietzeEquiv
Documentation

A free-group equivalence gives a Tietze equivalence between a relator set and its pullback relator set.

Source context 3 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
Lean source · statement
def freeGroupPullbackRelatorTietzeEquiv
    {X Y : Type*} (e : FreeGroup X ≃* FreeGroup Y)
    (S : Set (FreeGroup Y)) :
    TietzeEquiv (freeGroupPullbackRelatorSet e S) S
structure

Presentation

L234 ↗
ReidemeisterSchreier.Discrete.Presentations.Presentation
Documentation

A presentation packaged with its generator type. This is a light wrapper for writing long Tietze scripts whose intermediate presentations may have different generator types.

Source context 3 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
Lean source · full declaration
structure Presentation where
  /-- The type of generators of the presentation. -/
  Generator : Type u
  /-- The set of relators in the free group on `Generator`. -/
  relators : Set (FreeGroup Generator)
def

ofRelators

L243 ↗
ReidemeisterSchreier.Discrete.Presentations.Presentation.ofRelators
Documentation

This constructs a presentation from the given relator family.

Source context 4 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace Presentation
Lean source · full declaration
def ofRelators {X : Type u} (R : Set (FreeGroup X)) : Presentation.{u} where
  Generator := X
  relators := R
structure

PresentationEquivCertificate

L250 ↗
ReidemeisterSchreier.Discrete.Presentations.PresentationEquivCertificate
Documentation

A semantic equivalence certificate between packaged presentations.

Source context 3 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
Lean source · full declaration
structure PresentationEquivCertificate
    (P : Presentation.{u}) (Q : Presentation.{v}) where
  /-- The Tietze equivalence between the relator sets of the two presentations. -/
  toTietzeEquiv : TietzeEquiv P.relators Q.relators
def

ofTietzeEquiv

L261 ↗
ReidemeisterSchreier.Discrete.Presentations.PresentationEquivCertificate.ofTietzeEquiv
Documentation

A Tietze equivalence between the relator sets gives a scriptable Tietze certificate between the packaged presentations.

Source context 4 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace PresentationEquivCertificate
Lean source · full declaration
def ofTietzeEquiv {P : Presentation.{u}} {Q : Presentation.{v}}
    (D : TietzeEquiv P.relators Q.relators) :
    PresentationEquivCertificate P Q where
  toTietzeEquiv := D
def

ofMutualMapData

L267 ↗
ReidemeisterSchreier.Discrete.Presentations.PresentationEquivCertificate.ofMutualMapData
Documentation

Mutual maps modulo relators determine a Tietze script between the two presentations.

Source context 4 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace PresentationEquivCertificate
Lean source · statement
def ofMutualMapData {P : Presentation.{u}} {Q : Presentation.{v}}
    (D : RelatorQuotientMutualMapData P.relators Q.relators) :
    PresentationEquivCertificate P Q
def

refl

L273 ↗
ReidemeisterSchreier.Discrete.Presentations.PresentationEquivCertificate.refl
Documentation

Every packaged presentation has its identity semantic equivalence certificate.

Source context 4 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace PresentationEquivCertificate
Lean source · statement
def refl (P : Presentation.{u}) : PresentationEquivCertificate P P
def

symm

L277 ↗
ReidemeisterSchreier.Discrete.Presentations.PresentationEquivCertificate.symm
Documentation

Reversing a presentation certificate gives a certificate in the opposite direction.

Source context 4 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace PresentationEquivCertificate
Lean source · statement
def symm {P : Presentation.{u}} {Q : Presentation.{v}}
    (D : PresentationEquivCertificate P Q) :
    PresentationEquivCertificate Q P
def

trans

L283 ↗
ReidemeisterSchreier.Discrete.Presentations.PresentationEquivCertificate.trans
Documentation

Presentation equivalence certificates compose through an intermediate presentation.

Source context 4 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace PresentationEquivCertificate
Lean source · statement
def trans {P : Presentation.{u}} {Q : Presentation.{v}}
    {U : Presentation.{w}}
    (D₁ : PresentationEquivCertificate P Q) (D₂ : PresentationEquivCertificate Q U) :
    PresentationEquivCertificate P U
def

presentedEquiv

L290 ↗
ReidemeisterSchreier.Discrete.Presentations.PresentationEquivCertificate.presentedEquiv
Documentation

A Tietze script induces an isomorphism of the packaged presented groups.

Source context 4 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace PresentationEquivCertificate
Lean source · statement
def presentedEquiv
    {P : Presentation.{u}} {Q : Presentation.{v}}
    (D : PresentationEquivCertificate P Q) :
    PresentedGroup P.relators ≃* PresentedGroup Q.relators
def

quotientEquiv

L297 ↗
ReidemeisterSchreier.Discrete.Presentations.PresentationEquivCertificate.quotientEquiv
Documentation

A Tietze script induces an isomorphism of the packaged relator quotients.

Source context 4 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace PresentationEquivCertificate
Lean source · statement
def quotientEquiv
    {P : Presentation.{u}} {Q : Presentation.{v}}
    (D : PresentationEquivCertificate P Q) :
    FreeGroup P.Generator ⧸ Subgroup.normalClosure P.relators ≃*
      FreeGroup Q.Generator ⧸ Subgroup.normalClosure Q.relators
def

toCertificate

L309 ↗
ReidemeisterSchreier.Discrete.Presentations.TietzeEquiv.toCertificate
Documentation

Package a Tietze equivalence as a scriptable Tietze certificate.

Source context 4 commands

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

universe u v w
namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H K : Type*} [Group G] [Group H] [Group K]
namespace TietzeEquiv
Lean source · statement
def toCertificate
    {X Y : Type*} {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
    (D : TietzeEquiv R S) :
    PresentationEquivCertificate (Presentation.ofRelators R) (Presentation.ofRelators S)

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