English
Given isomorphisms f: D1 ≃* D2 and g: Q1 ≃* Q2, there is a corresponding isomorphism congr that transports D1 ≀ᵣ Q1 to D2 ≀ᵣ Q2.
Русский
Заданы изоморфизмы f: D1 ≃* D2 и g: Q1 ≃* Q2; имеется соответствующий изоморфизм congr между D1 ≀ᵣ Q1 и D2 ≀ᵣ Q2.
LaTeX
$${D₁ : Type*, Q₁ : Type*, D₂ : Type*, Q₂ : Type*} [Group D₁] [Group Q₁] [Group D₂] [Group Q₂] (f : D₁ ≃* D₂) (g : Q₁ ≃* Q₂) : D₁ ≀ᵣ Q₁ ≃* D₂ ≀ᵣ Q₂$$
Lean4
/-- Define an isomorphism from `D₁ ≀ᵣ Q₁` to `D₂ ≀ᵣ Q₂`
given isomorphisms `D₁ ≀ᵣ Q₁` and `Q₁ ≃* Q₂`. -/
def congr {D₁ Q₁ D₂ Q₂ : Type*} [Group D₁] [Group Q₁] [Group D₂] [Group Q₂] (f : D₁ ≃* D₂) (g : Q₁ ≃* Q₂) :
D₁ ≀ᵣ Q₁ ≃* D₂ ≀ᵣ Q₂ where
toFun x := ⟨f ∘ (x.left ∘ g.symm), g x.right⟩
invFun x := ⟨(f.symm ∘ x.left) ∘ g, g.symm x.right⟩
left_inv x := by ext <;> simp
right_inv x := by ext <;> simp
map_mul' x y := by ext <;> simp
