reindex_relationsSet — Mathlib

English

If e is a bijection of the index set, then reindexing M by e transports its set of relations via the corresponding free-group congruence.

Русский

Если e — биекция по индексному множеству, то перенормировка M по e переносит множество отношений через соответствующее конгруэнтное отображение свободной группы.

LaTeX

$$$ (M.\mathrm{reindex}\ e).\mathrm{relationsSet} = \mathrm{FreeGroup.freeGroupCongr}(e)''(M.\mathrm{relationsSet}) $$$

Lean4

theorem reindex_relationsSet : (M.reindex e).relationsSet = FreeGroup.freeGroupCongr e '' M.relationsSet :=
  let M' := M.reindex e;
  calc
    Set.range (uncurry M'.relation)
    _ = Set.range (uncurry M'.relation ∘ Prod.map e e) := by simp [Set.range_comp]
    _ = Set.range (FreeGroup.freeGroupCongr e ∘ uncurry M.relation) :=
      by
      apply congrArg Set.range
      ext ⟨i, i'⟩
      simp [relation, reindex_apply, M']
    _ = _ := by simp [Set.range_comp, relationsSet]

Похожие утверждения