mathlib documentation

algebra.category.Algebra.basic

Category instance for algebras over a commutative ring #

We introduce the bundled category Algebra of algebras over a fixed commutative ring R along with the forgetful functors to Ring and Module. We furthermore show that the functor associating to a type the free R-algebra on that type is left adjoint to the forgetful functor.

structure Algebra (R : Type u) [comm_ring R] :
Type (max u (v+1))

The category of R-algebras and their morphisms.

@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
def Algebra.of (R : Type u) [comm_ring R] (X : Type v) [ring X] [algebra R X] :

The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses.

Equations
@[instance]
def Algebra.inhabited (R : Type u) [comm_ring R] :
Equations
@[simp]
theorem Algebra.coe_of (R : Type u) [comm_ring R] (X : Type u) [ring X] [algebra R X] :
@[simp]
theorem Algebra.of_self_iso_hom {R : Type u} [comm_ring R] (M : Algebra R) :
@[simp]
theorem Algebra.of_self_iso_inv {R : Type u} [comm_ring R] (M : Algebra R) :
def Algebra.of_self_iso {R : Type u} [comm_ring R] (M : Algebra R) :

Forgetting to the underlying type and then building the bundled object returns the original algebra.

Equations
@[simp]
theorem Algebra.id_apply {R : Type u} [comm_ring R] {M : Module R} (m : M) :
(𝟙 M) m = m
@[simp]
theorem Algebra.coe_comp {R : Type u} [comm_ring R] {M N U : Module R} (f : M N) (g : N U) :
(f g) = g f
def Algebra.free (R : Type u) [comm_ring R] :
Type u_1 Algebra R

The "free algebra" functor, sending a type S to the free algebra on S.

Equations
@[simp]
theorem Algebra.free_obj_is_algebra (R : Type u) [comm_ring R] (S : Type u_1) :
@[simp]
theorem Algebra.free_obj_carrier (R : Type u) [comm_ring R] (S : Type u_1) :
@[simp]
theorem Algebra.free_obj_is_ring (R : Type u) [comm_ring R] (S : Type u_1) :
@[simp]
theorem Algebra.free_map (R : Type u) [comm_ring R] (S T : Type u_1) (f : S T) :

The free/forget ajunction for R-algebras.

Equations
@[simp]
theorem alg_equiv.to_Algebra_iso_hom {R : Type u} [comm_ring R] {X₁ X₂ : Type u} {g₁ : ring X₁} {g₂ : ring X₂} {m₁ : algebra R X₁} {m₂ : algebra R X₂} (e : X₁ ≃ₐ[R] X₂) :
def alg_equiv.to_Algebra_iso {R : Type u} [comm_ring R] {X₁ X₂ : Type u} {g₁ : ring X₁} {g₂ : ring X₂} {m₁ : algebra R X₁} {m₂ : algebra R X₂} (e : X₁ ≃ₐ[R] X₂) :
Algebra.of R X₁ Algebra.of R X₂

Build an isomorphism in the category Algebra R from a alg_equiv between algebras.

Equations
@[simp]
theorem alg_equiv.to_Algebra_iso_inv {R : Type u} [comm_ring R] {X₁ X₂ : Type u} {g₁ : ring X₁} {g₂ : ring X₂} {m₁ : algebra R X₁} {m₂ : algebra R X₂} (e : X₁ ≃ₐ[R] X₂) :
@[simp]
theorem category_theory.iso.to_alg_equiv_apply {R : Type u} [comm_ring R] {X Y : Algebra R} (i : X Y) (ᾰ : X) :
(i.to_alg_equiv) ᾰ = (i.hom) ᾰ
def category_theory.iso.to_alg_equiv {R : Type u} [comm_ring R] {X Y : Algebra R} (i : X Y) :

Build a alg_equiv from an isomorphism in the category Algebra R.

Equations
@[simp]
theorem category_theory.iso.to_alg_equiv_symm_apply {R : Type u} [comm_ring R] {X Y : Algebra R} (i : X Y) (ᾰ : Y) :
(i.to_alg_equiv.symm) ᾰ = (i.inv) ᾰ
@[simp]
theorem alg_equiv_iso_Algebra_iso_hom {R : Type u} [comm_ring R] {X Y : Type u} [ring X] [ring Y] [algebra R X] [algebra R Y] (e : X ≃ₐ[R] Y) :
def alg_equiv_iso_Algebra_iso {R : Type u} [comm_ring R] {X Y : Type u} [ring X] [ring Y] [algebra R X] [algebra R Y] :

Algebra equivalences between algebrass are the same as (isomorphic to) isomorphisms in Algebra.

Equations
@[simp]
theorem alg_equiv_iso_Algebra_iso_inv {R : Type u} [comm_ring R] {X Y : Type u} [ring X] [ring Y] [algebra R X] [algebra R Y] (i : Algebra.of R X Algebra.of R Y) :
@[instance]
def Algebra.has_coe {R : Type u} [comm_ring R] (X : Type u) [ring X] [algebra R X] :
Equations