From ade8889a3478cb4049fd8dce10a40e560065b42d Mon Sep 17 00:00:00 2001 From: tb65536 Date: Sun, 14 Mar 2021 03:22:08 +0000 Subject: [PATCH] feat(algebra/algebra/basic): An algebra isomorphism induces a group isomorphism between automorphism groups (#6622) Constructs the group isomorphism induced from an algebra isomorphism. Co-authored-by: tb65536 --- src/algebra/algebra/basic.lean | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean index bb927be9026ca..39534d64dd590 100644 --- a/src/algebra/algebra/basic.lean +++ b/src/algebra/algebra/basic.lean @@ -911,6 +911,25 @@ instance aut : group (A₁ ≃ₐ[R] A₁) := inv := symm, mul_left_inv := λ ϕ, by { ext, exact symm_apply_apply ϕ a } } +@[simp] lemma mul_apply (e₁ e₂ : A₁ ≃ₐ[R] A₁) (x : A₁) : (e₁ * e₂) x = e₁ (e₂ x) := rfl + +/-- An algebra isomorphism induces a group isomorphism between automorphism groups -/ +@[simps apply] +def aut_congr (ϕ : A₁ ≃ₐ[R] A₂) : (A₁ ≃ₐ[R] A₁) ≃* (A₂ ≃ₐ[R] A₂) := +{ to_fun := λ ψ, ϕ.symm.trans (ψ.trans ϕ), + inv_fun := λ ψ, ϕ.trans (ψ.trans ϕ.symm), + left_inv := λ ψ, by { ext, simp_rw [trans_apply, symm_apply_apply] }, + right_inv := λ ψ, by { ext, simp_rw [trans_apply, apply_symm_apply] }, + map_mul' := λ ψ χ, by { ext, simp only [mul_apply, trans_apply, symm_apply_apply] } } + +@[simp] lemma aut_congr_refl : aut_congr (alg_equiv.refl) = mul_equiv.refl (A₁ ≃ₐ[R] A₁) := +by { ext, refl } + +@[simp] lemma aut_congr_symm (ϕ : A₁ ≃ₐ[R] A₂) : (aut_congr ϕ).symm = aut_congr ϕ.symm := rfl + +@[simp] lemma aut_congr_trans (ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₂ ≃ₐ[R] A₃) : + (aut_congr ϕ).trans (aut_congr ψ) = aut_congr (ϕ.trans ψ) := rfl + end semiring section comm_semiring