mathlib documentation

algebra.category.Algebra.basic

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

The category of R-modules 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) :

@[simp]
theorem Algebra.adj_counit_app (R : Type u) [comm_ring R] (S : Algebra R) :

The free/forget ajunction for R-algebras.

Equations
@[simp]
theorem Algebra.adj_hom_equiv_to_fun (R : Type u) [comm_ring R] (X : Type (max u u_1)) (A : Algebra R) (f : (Algebra.free R).obj X A) (a : X) :

@[simp]
theorem Algebra.adj_hom_equiv_inv_fun (R : Type u) [comm_ring R] (X : Type (max u u_1)) (A : Algebra R) (f : X (category_theory.forget (Algebra R)).obj A) :

@[simp]
theorem Algebra.adj_unit_app (R : Type u) [comm_ring R] (S : Type (max u u_1)) (a : (𝟭 (Type (max u u_1))).obj S) :

@[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₂} :
(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_inv_fun {R : Type u} [comm_ring R] {X Y : Algebra R} (i : X Y) (a : Y) :

def category_theory.iso.to_alg_equiv {R : Type u} [comm_ring R] {X Y : Algebra R} :
(X Y)(X ≃ₐ[R] Y)

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

Equations
@[simp]
theorem category_theory.iso.to_alg_equiv_to_fun {R : Type u} [comm_ring R] {X Y : Algebra R} (i : X Y) (a : X) :

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