From 24572870b9eff53908c02b89a3ba6e0c316fc5cf Mon Sep 17 00:00:00 2001 From: tb65536 Date: Thu, 7 Jan 2021 10:05:33 +0000 Subject: [PATCH] feat(algebra/subalgebra): Restrict injective algebra homomorphism to algebra isomorphism (#5560) The domain of an injective algebra homomorphism is isomorphic to its range. --- src/algebra/algebra/subalgebra.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/algebra/algebra/subalgebra.lean b/src/algebra/algebra/subalgebra.lean index 27556b29779f5..2ac6bcf2a4903 100644 --- a/src/algebra/algebra/subalgebra.lean +++ b/src/algebra/algebra/subalgebra.lean @@ -298,6 +298,21 @@ theorem injective_cod_restrict (f : A →ₐ[R] B) (S : subalgebra R B) (hf : function.injective (f.cod_restrict S hf) ↔ function.injective f := ⟨λ H x y hxy, H $ subtype.eq hxy, λ H x y hxy, H (congr_arg subtype.val hxy : _)⟩ +/-- Restrict an injective algebra homomorphism to an algebra isomorphism -/ +noncomputable def alg_equiv.of_injective (f : A →ₐ[R] B) (hf : function.injective f) : + A ≃ₐ[R] f.range := +alg_equiv.of_bijective (f.cod_restrict f.range (λ x, f.mem_range.mpr ⟨x, rfl⟩)) +⟨(f.injective_cod_restrict f.range (λ x, f.mem_range.mpr ⟨x, rfl⟩)).mpr hf, + λ x, Exists.cases_on (f.mem_range.mp (subtype.mem x)) (λ y hy, ⟨y, subtype.ext hy⟩)⟩ + +@[simp] lemma alg_equiv.of_injective_apply (f : A →ₐ[R] B) (hf : function.injective f) (x : A) : + ↑(alg_equiv.of_injective f hf x) = f x := rfl + +/-- Restrict an algebra homomorphism between fields to an algebra isomorphism -/ +noncomputable def alg_equiv.of_injective_field {E F : Type*} [division_ring E] [semiring F] + [nontrivial F] [algebra R E] [algebra R F] (f : E →ₐ[R] F) : E ≃ₐ[R] f.range := +alg_equiv.of_injective f f.to_ring_hom.injective + /-- The equalizer of two R-algebra homomorphisms -/ def equalizer (ϕ ψ : A →ₐ[R] B) : subalgebra R A := { carrier := {a | ϕ a = ψ a},