ReidemeisterSchreier.Discrete.Presentations.Tietze.Core
This module develops the rewriting and basis constructions behind the subgroup calculations. It tracks words and relations through the chosen transversal to obtain the required presentation or basis statements.
import
- Mathlib.GroupTheory.PresentedGroup
- ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorMap
structure TietzeEquiv
{X Y : Type*} (R : Set (FreeGroup X)) (S : Set (FreeGroup Y)) where
toMutualMapData : RelatorQuotientMutualMapData R SA reusable Tietze certificate between two presentations. This is the scriptable layer: certificates can be reversed and composed while retaining the underlying normal-closure data.
def refl (R : Set (FreeGroup X)) : TietzeEquiv R R where
toMutualMapData := RelatorQuotientMutualMapData.refl RThe Tietze presentation identity follows from the prescribed generator and relator replacement maps.
def symm (D : TietzeEquiv R S) : TietzeEquiv S R where
toMutualMapData := D.toMutualMapData.symmThe Tietze presentation identity follows from the prescribed generator and relator replacement maps.
def trans (D₁ : TietzeEquiv R S) (D₂ : TietzeEquiv S T) :
TietzeEquiv R T where
toMutualMapData := D₁.toMutualMapData.trans D₂.toMutualMapDataThe Tietze presentation identity follows from the prescribed generator and relator replacement maps.
def ofMutualMapData (D : RelatorQuotientMutualMapData R S) :
TietzeEquiv R S where
toMutualMapData := DMutual relator-quotient map data define a Tietze equivalence.
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_RA Tietze equivalence is induced by a relator-equivalence comparison between the two relator sets.
def ofNormalClosureEq
{R S : Set (FreeGroup X)}
(h : Subgroup.normalClosure R = Subgroup.normalClosure S) :
TietzeEquiv R S where
toMutualMapData := relatorQuotientMutualMapDataOfNormalClosureEq hEqual normal closures give a Tietze equivalence between the two relator sets.
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 :=
TietzeEquiv.ofMutualMapData
(relatorQuotientMutualMapDataOfGeneratorMaps
toGenerator invGenerator hR hS hinv_to hto_inv)Compatible generator maps in both directions define a Tietze equivalence between the two relator quotients.
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 :=
TietzeEquiv.ofMutualMapData
(relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent
toGenerator invGenerator hR hS hinv_to hto_inv)Generator maps that preserve relators up to relator equivalence induce the corresponding presented-group map.
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) :=
TietzeEquiv.ofMutualMapData
(relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent_iUnion
toGenerator invGenerator hR hS hinv_to hto_inv)Tietze certificate from generator maps when both relator sets are indexed unions. Use this when a presentation has named relator families and each family has its own calculation.
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)noncomputable def quotientEquiv (D : TietzeEquiv R S) :
FreeGroup X ⧸ Subgroup.normalClosure R ≃*
FreeGroup Y ⧸ Subgroup.normalClosure S :=
quotientEquivOfRelatorQuotientMutualMapData R S D.toMutualMapDataA Tietze equivalence induces an isomorphism of the corresponding relator quotients.
noncomputable def presentedEquiv (D : TietzeEquiv R S) :
PresentedGroup R ≃* PresentedGroup S :=
quotientEquivOfRelatorQuotientMutualMapData R S D.toMutualMapDataA Tietze equivalence induces an isomorphism of presented groups.
def freeGroupPullbackRelatorTietzeEquiv
{X Y : Type*} (e : FreeGroup X ≃* FreeGroup Y)
(S : Set (FreeGroup Y)) :
TietzeEquiv (freeGroupPullbackRelatorSet e S) S :=
TietzeEquiv.ofMutualMapData
(relatorQuotientMutualMapDataOfNormalClosureMapEq
(freeGroupPullbackRelatorSet e S) S e
(map_normalClosure_freeGroupPullbackRelatorSet e S))A free-group equivalence gives a Tietze equivalence between a relator set and its pullback relator set.
def ofRelators {X : Type u} (R : Set (FreeGroup X)) : Presentation.{u} where
Generator := X
relators := RThis constructs a presentation from the given relator family.
structure TietzeScript (P : Presentation.{u}) (Q : Presentation.{v}) where
toTietzeEquiv : TietzeEquiv P.relators Q.relatorsA scriptable Tietze certificate between packaged presentations. The data is still exactly a TietzeEquiv; this wrapper only remembers the intermediate presentation objects so long chains can be composed without unpacking generator types by hand.
def ofTietzeEquiv {P : Presentation.{u}} {Q : Presentation.{v}}
(D : TietzeEquiv P.relators Q.relators) :
TietzeScript P Q where
toTietzeEquiv := DA Tietze equivalence between the relator sets gives a scriptable Tietze certificate between the packaged presentations.
def ofMutualMapData {P : Presentation.{u}} {Q : Presentation.{v}}
(D : RelatorQuotientMutualMapData P.relators Q.relators) :
TietzeScript P Q :=
ofTietzeEquiv (TietzeEquiv.ofMutualMapData D)Mutual maps modulo relators determine a Tietze script between the two presentations.
def refl (P : Presentation.{u}) : TietzeScript P P :=
ofTietzeEquiv (TietzeEquiv.refl P.relators)The Tietze presentation identity follows from the prescribed generator and relator replacement maps.
def symm {P : Presentation.{u}} {Q : Presentation.{v}}
(D : TietzeScript P Q) :
TietzeScript Q P :=
ofTietzeEquiv D.toTietzeEquiv.symmThe Tietze presentation identity follows from the prescribed generator and relator replacement maps.
def trans {P : Presentation.{u}} {Q : Presentation.{v}}
{U : Presentation.{w}}
(D₁ : TietzeScript P Q) (D₂ : TietzeScript Q U) :
TietzeScript P U :=
ofTietzeEquiv (D₁.toTietzeEquiv.trans D₂.toTietzeEquiv)The Tietze presentation identity follows from the prescribed generator and relator replacement maps.
noncomputable def presentedEquiv
{P : Presentation.{u}} {Q : Presentation.{v}}
(D : TietzeScript P Q) :
PresentedGroup P.relators ≃* PresentedGroup Q.relators :=
D.toTietzeEquiv.presentedEquivA Tietze script induces an isomorphism of the packaged presented groups.
noncomputable def quotientEquiv
{P : Presentation.{u}} {Q : Presentation.{v}}
(D : TietzeScript P Q) :
FreeGroup P.Generator ⧸ Subgroup.normalClosure P.relators ≃*
FreeGroup Q.Generator ⧸ Subgroup.normalClosure Q.relators :=
D.toTietzeEquiv.quotientEquivA Tietze script induces an isomorphism of the packaged relator quotients.
def toScript
{X Y : Type*} {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
(D : TietzeEquiv R S) :
TietzeScript (Presentation.ofRelators R) (Presentation.ofRelators S) :=
TietzeScript.ofTietzeEquiv DPackage a Tietze equivalence as a scriptable Tietze certificate.