unitsSMul_one_group_smul — Mathlib

English

There is a natural action of the HNN extension on the words by left multiplication, making NormalWord into a module over the HNN extension.

Русский

Существует естественное действие HNN-расширения на слова слева, превращающее NormalWord в модуль над HNN-расширением.

LaTeX

$$$\\text{instMulAction}_1 : \\text{MulAction} \\; (\\mathrm{HNNExtension}\\; G\\; A\\; B\\; \\varphi)\\; (\\text{NormalWord } d).$$$

Lean4

theorem unitsSMul_one_group_smul (g : A) (w : NormalWord d) :
    unitsSMul φ 1 ((g : G) • w) = (φ g : G) • (unitsSMul φ 1 w) :=
  by
  unfold unitsSMul
  have : Cancels 1 ((g : G) • w) ↔ Cancels 1 w := by simp [Cancels, Subgroup.mul_mem_cancel_left]
  by_cases hcan : Cancels 1 w
  · simp only [unitsSMulWithCancel, toSubgroup_one, id_eq, toSubgroup_neg_one, toSubgroupEquiv_one, group_smul_head,
      mul_inv_rev, dif_pos (this.2 hcan), dif_pos hcan]
    cases w using consRecOn
    · simp [Cancels] at hcan
    · simp only [smul_cons, consRecOn_cons]
      rw [← mul_smul, ← Subgroup.coe_mul, ← map_mul φ]
      rfl
  · rw [dif_neg (mt this.1 hcan), dif_neg hcan]
      -- Before https://github.com/leanprover/lean4/pull/2644, all this was just
          -- `simp [← mul_smul, mul_assoc, unitsSMulGroup]`

    simp only [toSubgroup_neg_one, unitsSMulGroup, toSubgroup_one, toSubgroupEquiv_one, SetLike.coe_sort_coe,
      group_smul_head, mul_inv_rev, ← mul_smul, mul_assoc, inv_mul_cancel, mul_one, smul_cons]
      -- This used to be the end of the proof before https://github.com/leanprover/lean4/pull/2644

    congr 1
    · conv_lhs => erw [IsComplement.equiv_mul_left]
      simp_rw [toSubgroup_one]
      simp only [SetLike.coe_sort_coe, map_mul, Subgroup.coe_mul]
    conv_lhs => erw [IsComplement.equiv_mul_left]
    rfl

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