Local algebra homomorphisms #
We prove basic properties of local algebra homomorphisms.
theorem
AlgHom.isLocalHom_of_isLocalHom_toRingHom
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Algebra R A]
[Algebra R B]
(f : A →ₐ[R] B)
[h : IsLocalHom f.toRingHom]
:
@[instance 100]
instance
AlgHom.isLocalHom_of_isLocalHom_AlgHom
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Algebra R A]
[Algebra R B]
(f : A →ₐ[R] B)
[IsLocalHom f]
:
instance
AlgHom.isLocalHom_id
{R : Type u_1}
[CommSemiring R]
(X : Type u_5)
[Semiring X]
[Algebra R X]
:
IsLocalHom (AlgHom.id R X)
@[instance 100]
instance
AlgHom.isLocalAlgHomtoAlgHom
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Algebra R A]
[Algebra R B]
{F : Type u_5}
[FunLike F A B]
[AlgHomClass F R A B]
(f : F)
[IsLocalHom f]
:
IsLocalHom ↑f
instance
AlgHom.isLocalHom_comp
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{C : Type u_4}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Semiring C]
[Algebra R A]
[Algebra R B]
[Algebra R C]
(g : B →ₐ[R] C)
(f : A →ₐ[R] B)
[IsLocalHom g]
[IsLocalHom f]
:
IsLocalHom (g.comp f)