English
A multiplicative variant of arrowCongr: given a base equivalence f : M ≃ N and a multiplicative equivalence g : P ≃* Q, there is a multiplicative equivalence between function types M → P and N → Q defined by h ↦ g ∘ h ∘ f⁻¹.
Русский
Мульти-эквивалентное аналогия arrowCongr: имея эквивалентность f : M ≃ N и умножительную эквивалентность g : P ≃* Q, существует умножительная эквивалентность между функциями M → P и N → Q, задаваемая h ↦ g ∘ h ∘ f⁻¹.
LaTeX
$$$ (M \to P) \;\cong^*\; (N \to Q) \quad \text{via } (h \mapsto g \circ h \circ f^{-1}, \; k \mapsto g^{-1} \circ k \circ f). $$$
Lean4
/-- A multiplicative analogue of `Equiv.arrowCongr`,
where the equivalence between the targets is multiplicative.
-/
@[to_additive (attr := simps apply) /-- An additive analogue of `Equiv.arrowCongr`,
where the equivalence between the targets is additive. -/
]
def arrowCongr {M N P Q : Type*} [Mul P] [Mul Q] (f : M ≃ N) (g : P ≃* Q) : (M → P) ≃* (N → Q)
where
toFun h n := g (h (f.symm n))
invFun k m := g.symm (k (f m))
left_inv h := by ext; simp
right_inv k := by ext; simp
map_mul' h k := by ext; simp
