@[instance]
Equations
- Algebra.has_coe_to_sort R = {S := Type u, coe := Algebra.carrier _inst_1}
@[instance]
Equations
- Algebra.category_theory.category R = {to_category_struct := {to_has_hom := {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' := _}
@[instance]
@[instance]
@[instance]
def
Algebra.has_forget_to_Module
(R : Type u)
[comm_ring R] :
category_theory.has_forget₂ (Algebra R) (Module R)
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
@[instance]
Equations
- Algebra.inhabited R = {default := Algebra.of R R (algebra.id R)}
@[simp]
theorem
Algebra.of_apply
(R : Type u)
[comm_ring R]
(X : Type u)
[ring X]
[algebra R X] :
↥(Algebra.of R X) = X
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.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
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
- e.to_Algebra_iso = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
Build a alg_equiv from an isomorphism in the category Algebra R.
@[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) :
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' := _}
@[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}
@[instance]
Equations
- Algebra.forget_reflects_isos = {reflects := λ (X Y : Algebra R) (f : X ⟶ Y) (_x : category_theory.is_iso ((category_theory.forget (Algebra R)).map f)), let i : (category_theory.forget (Algebra R)).obj X ≅ (category_theory.forget (Algebra R)).obj Y := category_theory.as_iso ((category_theory.forget (Algebra R)).map f), e : ↥X ≃ₐ[R] ↥Y := {to_fun := f.to_fun, inv_fun := i.to_equiv.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _} in {inv := e.to_Algebra_iso.inv, hom_inv_id' := _, inv_hom_id' := _}}