Yamaguchi Lean 4 Library
ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Congruence
ProCGroups/ReidemeisterSchreier/Discrete/Presentations/Relators/Congruence

ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Congruence

17 Theorems

This module transports normal-closure membership and relator equivalence through inclusions, homomorphisms, and indexed unions of relator families.

import
Imported by

Declarations

Theorem ReidemeisterSchreier.Discrete.Presentations.mem_normalClosure_of_subset 
theorem mem_normalClosure_of_subset
    (hR_to_S : R ⊆ S) {x : G}
    (hx : x ∈ Subgroup.normalClosure R) :
    x ∈ Subgroup.normalClosure S

Membership in a normal closure is preserved when the relator set is enlarged.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.mem_normalClosure_union_left 
theorem mem_normalClosure_union_left
    {x : G} (hx : x ∈ Subgroup.normalClosure R) :
    x ∈ Subgroup.normalClosure (R ∪ S)

Membership in the left normal closure implies membership in the normal closure of the union.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.mem_normalClosure_union_right 
theorem mem_normalClosure_union_right
    {x : G} (hx : x ∈ Subgroup.normalClosure S) :
    x ∈ Subgroup.normalClosure (R ∪ S)

Membership in the right normal closure implies membership in the normal closure of the union.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.mem_normalClosure_iUnion 
theorem mem_normalClosure_iUnion
    {ι : Sort*} (R : ι → Set G) (i : ι)
    {x : G} (hx : x ∈ Subgroup.normalClosure (R i)) :
    x ∈ Subgroup.normalClosure (Set.iUnion R)

Membership in one indexed normal closure implies membership in the normal closure of the indexed union.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.mem_normalClosure_iUnion₂ 
theorem mem_normalClosure_iUnion₂
    {ι : Sort*} {κ : ι → Sort*}
    (R : ∀ i : ι, κ i → Set G) (i : ι) (j : κ i)
    {x : G} (hx : x ∈ Subgroup.normalClosure (R i j)) :
    x ∈ Subgroup.normalClosure
        (Set.iUnion fun i : ι => Set.iUnion (R i))

Membership in one doubly indexed normal closure implies membership in the normal closure of the doubly indexed union.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.mem_normalClosure_iUnion₂_of_exists 
theorem mem_normalClosure_iUnion₂_of_exists
    {ι : Sort*} {κ : ι → Sort*}
    (R : ∀ i : ι, κ i → Set G)
    {x : G} (hx : ∃ i : ι, ∃ j : κ i,
      x ∈ Subgroup.normalClosure (R i j)) :
    x ∈ Subgroup.normalClosure
        (Set.iUnion fun i : ι => Set.iUnion (R i))

An explicit pair of indices gives membership in the normal closure of the doubly indexed union.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.maps_iUnion_relators_mem_normalClosure 
theorem maps_iUnion_relators_mem_normalClosure
    {ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
    (hR : ∀ i : ι, ∀ r ∈ R i, f r ∈ Subgroup.normalClosure S) :
    ∀ r ∈ Set.iUnion R, f r ∈ Subgroup.normalClosure S

Maps that preserve each indexed relator family send the union of the source relators into the target normal closure.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.maps_iUnion₂_relators_mem_normalClosure 
theorem maps_iUnion₂_relators_mem_normalClosure
    {ι : Sort*} {κ : ι → Sort*}
    (f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
    (hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
      f r ∈ Subgroup.normalClosure S) :
    ∀ r ∈ Set.iUnion (fun i : ι => Set.iUnion (R i)),
      f r ∈ Subgroup.normalClosure S

Maps that preserve each doubly indexed relator family send the union of the source relators into the target normal closure.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.map_mem_normalClosure_of_relators 
theorem map_mem_normalClosure_of_relators
    (f : G →* H) {R : Set G} {S : Set H}
    (hR : ∀ r ∈ R, f r ∈ Subgroup.normalClosure S)
    {x : G} (hx : x ∈ Subgroup.normalClosure R) :
    f x ∈ Subgroup.normalClosure S

A relator-preserving map sends relators into the normal closure of the target relator set.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.hom_relatorEquivalent_of_maps_relators 
theorem hom_relatorEquivalent_of_maps_relators
    (f : G →* H) {R : Set G} {S : Set H}
    (hR : ∀ r ∈ R, f r ∈ Subgroup.normalClosure S)
    {u v : G} (h : RelatorEquivalent R u v) :
    RelatorEquivalent S (f u) (f v)

A homomorphism preserves relator equivalence when each source relator maps into the target normal closure.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.hom_relatorEquivalent_of_maps_relators_relatorEquivalent 
theorem hom_relatorEquivalent_of_maps_relators_relatorEquivalent
    (f : G →* H) {R : Set G} {S : Set H}
    (hR : ∀ r ∈ R, RelatorEquivalent S (f r) 1)
    {u v : G} (h : RelatorEquivalent R u v) :
    RelatorEquivalent S (f u) (f v)

A homomorphism preserves relator equivalence when each source relator maps to a target-relator-equivalent trivial word.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.map_mem_normalClosure_iUnion_of_relators 
theorem map_mem_normalClosure_iUnion_of_relators
    {ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
    (hR : ∀ i : ι, ∀ r ∈ R i, f r ∈ Subgroup.normalClosure S)
    {x : G} (hx : x ∈ Subgroup.normalClosure (Set.iUnion R)) :
    f x ∈ Subgroup.normalClosure S

A mapped relator from an indexed family lies in the normal closure of the union of the mapped relator families.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.map_mem_normalClosure_iUnion₂_of_relators 
theorem map_mem_normalClosure_iUnion₂_of_relators
    {ι : Sort*} {κ : ι → Sort*}
    (f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
    (hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
      f r ∈ Subgroup.normalClosure S)
    {x : G}
    (hx : x ∈ Subgroup.normalClosure
      (Set.iUnion fun i : ι => Set.iUnion (R i))) :
    f x ∈ Subgroup.normalClosure S

A mapped relator from a doubly indexed family lies in the normal closure of the union of the mapped relator families.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.hom_relatorEquivalent_of_maps_iUnion_relators 
theorem hom_relatorEquivalent_of_maps_iUnion_relators
    {ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
    (hR : ∀ i : ι, ∀ r ∈ R i, f r ∈ Subgroup.normalClosure S)
    {u v : G} (h : RelatorEquivalent (Set.iUnion R) u v) :
    RelatorEquivalent S (f u) (f v)

A homomorphism preserves relator equivalence for an indexed union of relators when every source relator maps into the target normal closure.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.hom_relatorEquivalent_of_maps_iUnion_relators_relatorEquivalent 
theorem hom_relatorEquivalent_of_maps_iUnion_relators_relatorEquivalent
    {ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
    (hR : ∀ i : ι, ∀ r ∈ R i, RelatorEquivalent S (f r) 1)
    {u v : G} (h : RelatorEquivalent (Set.iUnion R) u v) :
    RelatorEquivalent S (f u) (f v)

A homomorphism preserves relator equivalence for an indexed union of relators when every source relator maps to a target-relator-equivalent trivial word.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.hom_relatorEquivalent_of_maps_iUnion₂_relators 
theorem hom_relatorEquivalent_of_maps_iUnion₂_relators
    {ι : Sort*} {κ : ι → Sort*}
    (f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
    (hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
      f r ∈ Subgroup.normalClosure S)
    {u v : G}
    (h : RelatorEquivalent
      (Set.iUnion fun i : ι => Set.iUnion (R i)) u v) :
    RelatorEquivalent S (f u) (f v)

A homomorphism preserves relator equivalence for a doubly indexed union of relators when every source relator maps into the target normal closure.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.hom_relatorEquivalent_of_maps_iUnion₂_relators_relatorEquivalent 
theorem hom_relatorEquivalent_of_maps_iUnion₂_relators_relatorEquivalent
    {ι : Sort*} {κ : ι → Sort*}
    (f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
    (hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
      RelatorEquivalent S (f r) 1)
    {u v : G}
    (h : RelatorEquivalent
      (Set.iUnion fun i : ι => Set.iUnion (R i)) u v) :
    RelatorEquivalent S (f u) (f v)

A homomorphism preserves relator equivalence for a doubly indexed union of relators when every source relator maps to a target-relator-equivalent trivial word.

Show Lean proof