English
A similar compatibility holds for the first component when combining g1 and g2 with S-elements, showing how the 'fst' channel behaves under multiplication.
Русский
Аналогичная совместимость сохраняется для первого компонента при комбинировании g1 и g2 с элементами S, показывая как ведет себя канал 'fst' при умножении.
LaTeX
$$$indToCoindAux A (s \cdot g1) (A.ρ s a) g2 = indToCoindAux A g1 a g2$$$
Lean4
@[simp]
theorem indToCoindAux_mul_fst (g₁ g₂ : G) (a : A) (s : S) :
indToCoindAux A (s * g₁) (A.ρ s a) g₂ = indToCoindAux A g₁ a g₂ :=
by
rcases em ((QuotientGroup.rightRel S).r g₂ g₁) with ⟨s₁, rfl⟩ | h
· simp only [indToCoindAux, LinearMap.pi_apply]
rw [dif_pos ⟨s₁ * s⁻¹, by simp [S.1.smul_def, smul_eq_mul, mul_assoc]⟩, dif_pos ⟨s₁, rfl⟩, ← Module.End.mul_apply, ←
map_mul]
congr
simp [Subtype.ext_iff, S.1.smul_def, mul_assoc]
· rw [indToCoindAux_of_not_rel (h := h), indToCoindAux_of_not_rel]
exact mt (fun ⟨s₁, hs₁⟩ => ⟨s₁ * s, by simp_all [S.1.smul_def, mul_assoc]⟩) h
