mathlib3 documentation

algebra.category.Algebra.basic

Category instance for algebras over a commutative ring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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))

carrier : Type ?
is_ring : ring self.carrier
is_algebra : algebra R self.carrier

The category of R-algebras and their morphisms.

Instances for Algebra

Algebra.has_sizeof_inst
Algebra.has_coe_to_sort
Algebra.category_theory.category
Algebra.category_theory.concrete_category
Algebra.has_forget_to_Ring
Algebra.has_forget_to_Module
Algebra.inhabited
Algebra.has_coe
Cliff.has_forget_to_Algebra

@[protected, instance]

def Algebra.has_coe_to_sort (R : Type u) [comm_ring R] :

has_coe_to_sort (Algebra R) (Type v)

Equations

Algebra.has_coe_to_sort R = {coe := Algebra.carrier _inst_1}

@[protected, instance]

def Algebra.category_theory.category (R : Type u) [comm_ring R] :

category_theory.category (Algebra R)

Equations

Algebra.category_theory.category R = {to_category_struct := {to_quiver := {hom := λ (A B : Algebra R), ↥A →ₐ[R] ↥B}, id := λ (A : Algebra R), alg_hom.id R ↥A, comp := λ (A B C : Algebra R) (f : A ⟶ B) (g : B ⟶ C), alg_hom.comp g f}, id_comp' := _, comp_id' := _, assoc' := _}

@[protected, instance]

def Algebra.category_theory.concrete_category (R : Type u) [comm_ring R] :

category_theory.concrete_category (Algebra R)

Equations

Algebra.category_theory.concrete_category R = category_theory.concrete_category.mk {obj := λ (R_1 : Algebra R), ↥R_1, map := λ (R_1 S : Algebra R) (f : R_1 ⟶ S), ⇑f, map_id' := _, map_comp' := _}

@[protected, instance]

def Algebra.has_forget_to_Ring (R : Type u) [comm_ring R] :

category_theory.has_forget₂ (Algebra R) Ring

Equations

Algebra.has_forget_to_Ring R = {forget₂ := {obj := λ (A : Algebra R), Ring.of ↥A, map := λ (A₁ A₂ : Algebra R) (f : A₁ ⟶ A₂), alg_hom.to_ring_hom f, map_id' := _, map_comp' := _}, forget_comp := _}

@[protected, instance]

def Algebra.has_forget_to_Module (R : Type u) [comm_ring R] :

category_theory.has_forget₂ (Algebra R) (Module R)

Equations

Algebra.has_forget_to_Module R = {forget₂ := {obj := λ (M : Algebra R), Module.of R ↥M, map := λ (M₁ M₂ : Algebra R) (f : M₁ ⟶ M₂), alg_hom.to_linear_map f, map_id' := _, map_comp' := _}, forget_comp := _}

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

Algebra.of R X = Algebra.mk X

def Algebra.of_hom {R : Type u} [comm_ring R] {X Y : Type v} [ring X] [algebra R X] [ring Y] [algebra R Y] (f : X →ₐ[R] Y) :

Algebra.of R X ⟶ Algebra.of R Y

Typecheck a alg_hom as a morphism in Algebra R.

Equations

Algebra.of_hom f = f

@[simp]

theorem Algebra.of_hom_apply {R : Type u} [comm_ring R] {X Y : Type v} [ring X] [algebra R X] [ring Y] [algebra R Y] (f : X →ₐ[R] Y) (x : X) :

⇑(Algebra.of_hom f) x = ⇑f x

@[protected, instance]

def Algebra.inhabited (R : Type u) [comm_ring R] :

inhabited (Algebra R)

Equations

Algebra.inhabited R = {default := Algebra.of R R (algebra.id R)}

@[simp]

theorem Algebra.coe_of (R : Type u) [comm_ring R] (X : Type u) [ring X] [algebra R X] :

↥(Algebra.of R X) = X

@[simp]

theorem Algebra.of_self_iso_hom {R : Type u} [comm_ring R] (M : Algebra R) :

M.of_self_iso.hom = 𝟙 M

@[simp]

theorem Algebra.of_self_iso_inv {R : Type u} [comm_ring R] (M : Algebra R) :

M.of_self_iso.inv = 𝟙 M

def Algebra.of_self_iso {R : Type u} [comm_ring R] (M : Algebra R) :

Algebra.of R ↥M ≅ M

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

Equations

M.of_self_iso = {hom := 𝟙 M, inv := 𝟙 M, hom_inv_id' := _, inv_hom_id' := _}

@[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 ⥤ Algebra R

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

Equations

Algebra.free R = {obj := λ (S : Type u), Algebra.mk (free_algebra R S), map := λ (S T : Type u) (f : S ⟶ T), ⇑(free_algebra.lift R) (free_algebra.ι R ∘ f), map_id' := _, map_comp' := _}

@[simp]

theorem Algebra.free_obj_is_algebra (R : Type u) [comm_ring R] (S : Type u) :

((Algebra.free R).obj S).is_algebra = free_algebra.algebra R S

@[simp]

theorem Algebra.free_obj_carrier (R : Type u) [comm_ring R] (S : Type u) :

↥((Algebra.free R).obj S) = free_algebra R S

@[simp]

theorem Algebra.free_obj_is_ring (R : Type u) [comm_ring R] (S : Type u) :

((Algebra.free R).obj S).is_ring = algebra.semiring_to_ring R

@[simp]

theorem Algebra.free_map (R : Type u) [comm_ring R] (S T : Type u) (f : S ⟶ T) :

(Algebra.free R).map f = ⇑(free_algebra.lift R) (free_algebra.ι R ∘ f)

def Algebra.adj (R : Type u) [comm_ring R] :

Algebra.free R ⊣ category_theory.forget (Algebra R)

The free/forget adjunction for R-algebras.

Equations

Algebra.adj R = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : Type u) (A : Algebra R), (free_algebra.lift R).symm, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}

@[protected, instance]

def Algebra.category_theory.forget.category_theory.is_right_adjoint (R : Type u) [comm_ring R] :

category_theory.is_right_adjoint (category_theory.forget (Algebra R))

Equations

Algebra.category_theory.forget.category_theory.is_right_adjoint R = {left := Algebra.free R _inst_1, adj := Algebra.adj R _inst_1}

@[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₂) :

e.to_Algebra_iso.hom = ↑e

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

e.to_Algebra_iso = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}

@[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₂) :

e.to_Algebra_iso.inv = ↑(e.symm)

@[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) :

↥X ≃ₐ[R] ↥Y

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

Equations

i.to_alg_equiv = {to_fun := ⇑(i.hom), inv_fun := ⇑(i.inv), left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

@[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) :

alg_equiv_iso_Algebra_iso.hom e = e.to_Algebra_iso

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] :

(X ≃ₐ[R] Y) ≅ Algebra.of R X ≅ Algebra.of R Y

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

Equations

alg_equiv_iso_Algebra_iso = {hom := λ (e : X ≃ₐ[R] Y), e.to_Algebra_iso, inv := λ (i : Algebra.of R X ≅ Algebra.of R Y), i.to_alg_equiv, hom_inv_id' := _, inv_hom_id' := _}

@[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) :

alg_equiv_iso_Algebra_iso.inv i = i.to_alg_equiv

@[protected, instance]

def Algebra.has_coe {R : Type u} [comm_ring R] (X : Type u) [ring X] [algebra R X] :

has_coe (subalgebra R X) (Algebra R)

Equations

Algebra.has_coe X = {coe := λ (N : subalgebra R X), Algebra.of R ↥N}

@[protected, instance]

def Algebra.forget_reflects_isos {R : Type u} [comm_ring R] :

category_theory.reflects_isomorphisms (category_theory.forget (Algebra R))