Category instance for algebras over a commutative ring

We introduce the bundled category AlgCat of algebras over a fixed commutative ring R along with the forgetful functors to RingCat and ModuleCat. 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 AlgCat (R : Type u) [CommRing R] : Type (max u (v + 1))

The category of R-algebras and their morphisms.

• carrier : Type v

  The underlying type.

• isRing : Ring ↑self
• isAlgebra : Algebra R ↑self

@[implicit_reducible]

instance AlgCat.instCoeSortType (R : Type u) [CommRing R] : CoeSort (AlgCat R) (Type v)

@[reducible, inline]

abbrev AlgCat.of (R : Type u) [CommRing R] (X : Type v) [Ring X] [Algebra R X] : AlgCat R

The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses. This is the preferred way to construct a term of AlgCat R.

theorem AlgCat.coe_of (R : Type u) [CommRing R] (X : Type v) [Ring X] [Algebra R X] : ↑(of R X) = X

structure AlgCat.Hom {R : Type u} [CommRing R] (A B : AlgCat R) : Type v

The type of morphisms in AlgCat R.

• hom' : ↑A →ₐ[R] ↑B

  The underlying algebra map.

theorem AlgCat.Hom.ext {R : Type u} {inst✝ : CommRing R} {A B : AlgCat R} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

theorem AlgCat.Hom.ext_iff {R : Type u} {inst✝ : CommRing R} {A B : AlgCat R} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'

@[implicit_reducible]

instance AlgCat.instCategory (R : Type u) [CommRing R] : CategoryTheory.Category.{v, max (v + 1) u} (AlgCat R)

@[implicit_reducible]

instance AlgCat.instConcreteCategoryAlgHomCarrier (R : Type u) [CommRing R] : CategoryTheory.ConcreteCategory (AlgCat R) fun (x1 x2 : AlgCat R) => ↑x1 →ₐ[R] ↑x2

@[reducible, inline]

abbrev AlgCat.Hom.hom {R : Type u} [CommRing R] {A B : AlgCat R} (f : A.Hom B) : ↑A →ₐ[R] ↑B

Turn a morphism in AlgCat back into an AlgHom.

@[reducible, inline]

abbrev AlgCat.ofHom {R : Type u} [CommRing R] {A B : Type v} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : of R A ⟶ of R B

Typecheck an AlgHom as a morphism in AlgCat.

def AlgCat.Hom.Simps.hom {R : Type u} [CommRing R] (A B : AlgCat R) (f : A.Hom B) : ↑A →ₐ[R] ↑B

Use the ConcreteCategory.hom projection for @[simps] lemmas.

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

theorem AlgCat.hom_id (R : Type u) [CommRing R] {A : AlgCat R} : Hom.hom (CategoryTheory.CategoryStruct.id A) = AlgHom.id R ↑A

theorem AlgCat.id_apply (R : Type u) [CommRing R] (A : AlgCat R) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id A)) a = a

@[simp]

theorem AlgCat.hom_comp (R : Type u) [CommRing R] {A B C : AlgCat R} (f : A ⟶ B) (g : B ⟶ C) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem AlgCat.comp_apply (R : Type u) [CommRing R] {A B C : AlgCat R} (f : A ⟶ B) (g : B ⟶ C) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) a = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) a)

theorem AlgCat.hom_ext (R : Type u) [CommRing R] {A B : AlgCat R} {f g : A ⟶ B} (hf : Hom.hom f = Hom.hom g) : f = g

theorem AlgCat.hom_ext_iff {R : Type u} [CommRing R] {A B : AlgCat R} {f g : A ⟶ B} : f = g ↔ Hom.hom f = Hom.hom g

@[simp]

theorem AlgCat.hom_ofHom {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Algebra R X] [Ring Y] [Algebra R Y] (f : X →ₐ[R] Y) : Hom.hom (ofHom f) = f

@[simp]

theorem AlgCat.ofHom_hom (R : Type u) [CommRing R] {A B : AlgCat R} (f : A ⟶ B) : ofHom (Hom.hom f) = f

@[simp]

theorem AlgCat.ofHom_id (R : Type u) [CommRing R] {X : Type v} [Ring X] [Algebra R X] : ofHom (AlgHom.id R X) = CategoryTheory.CategoryStruct.id (of R X)

@[simp]

theorem AlgCat.ofHom_comp (R : Type u) [CommRing R] {X Y Z : Type v} [Ring X] [Ring Y] [Ring Z] [Algebra R X] [Algebra R Y] [Algebra R Z] (f : X →ₐ[R] Y) (g : Y →ₐ[R] Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem AlgCat.ofHom_apply {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Algebra R X] [Ring Y] [Algebra R Y] (f : X →ₐ[R] Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem AlgCat.inv_hom_apply (R : Type u) [CommRing R] {A B : AlgCat R} (e : A ≅ B) (x : ↑A) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem AlgCat.hom_inv_apply (R : Type u) [CommRing R] {A B : AlgCat R} (e : A ≅ B) (x : ↑B) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) x) = x

@[implicit_reducible]

instance AlgCat.instInhabited (R : Type u) [CommRing R] : Inhabited (AlgCat R)

theorem AlgCat.forget_obj (R : Type u) [CommRing R] {A : AlgCat R} : (CategoryTheory.forget (AlgCat R)).obj A = ↑A

theorem AlgCat.forget_map (R : Type u) [CommRing R] {A B : AlgCat R} (f : A ⟶ B) : (CategoryTheory.forget (AlgCat R)).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

@[implicit_reducible]

instance AlgCat.instRingObjForgetAlgHomCarrier (R : Type u) [CommRing R] {S : AlgCat R} : Ring ((CategoryTheory.forget (AlgCat R)).obj S)

@[implicit_reducible]

instance AlgCat.instAlgebraObjForgetAlgHomCarrier (R : Type u) [CommRing R] {S : AlgCat R} : Algebra R ((CategoryTheory.forget (AlgCat R)).obj S)

@[implicit_reducible]

instance AlgCat.hasForgetToRing (R : Type u) [CommRing R] : CategoryTheory.HasForget₂ (AlgCat R) RingCat

@[implicit_reducible]

instance AlgCat.hasForgetToModule (R : Type u) [CommRing R] : CategoryTheory.HasForget₂ (AlgCat R) (ModuleCat R)

@[simp]

theorem AlgCat.forget₂_module_obj (R : Type u) [CommRing R] (X : AlgCat R) : (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj X = ModuleCat.of R ↑X

@[simp]

theorem AlgCat.forget₂_module_map (R : Type u) [CommRing R] {X Y : AlgCat R} (f : X ⟶ Y) : (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).map f = ModuleCat.ofHom (Hom.hom f).toLinearMap

def AlgCat.free (R : Type u) [CommRing R] : CategoryTheory.Functor (Type u) (AlgCat R)

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

@[simp]

theorem AlgCat.free_map (R : Type u) [CommRing R] {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) : (free R).map f = ofHom ((FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f))

@[simp]

theorem AlgCat.free_obj (R : Type u) [CommRing R] (S : Type u) : (free R).obj S = of R (FreeAlgebra R S)

def AlgCat.adj (R : Type u) [CommRing R] : free R ⊣ CategoryTheory.forget (AlgCat R)

The free/forget adjunction for R-algebras.

instance AlgCat.instIsRightAdjointForgetAlgHomCarrier (R : Type u) [CommRing R] : (CategoryTheory.forget (AlgCat R)).IsRightAdjoint

def AlgEquiv.toAlgebraIso {R : Type u} [CommRing R] {X₁ X₂ : Type u} {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra R X₁} {m₂ : Algebra R X₂} (e : X₁ ≃ₐ[R] X₂) : AlgCat.of R X₁ ≅ AlgCat.of R X₂

Build an isomorphism in the category AlgCat R from an AlgEquiv between Algebras.

@[simp]

theorem AlgEquiv.toAlgebraIso_inv {R : Type u} [CommRing R] {X₁ X₂ : Type u} {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra R X₁} {m₂ : Algebra R X₂} (e : X₁ ≃ₐ[R] X₂) : e.toAlgebraIso.inv = AlgCat.ofHom ↑e.symm

@[simp]

theorem AlgEquiv.toAlgebraIso_hom {R : Type u} [CommRing R] {X₁ X₂ : Type u} {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra R X₁} {m₂ : Algebra R X₂} (e : X₁ ≃ₐ[R] X₂) : e.toAlgebraIso.hom = AlgCat.ofHom ↑e

def CategoryTheory.Iso.toAlgEquiv {R : Type u} [CommRing R] {X Y : AlgCat R} (i : X ≅ Y) : ↑X ≃ₐ[R] ↑Y

Build an AlgEquiv from an isomorphism in the category AlgCat R.

@[simp]

theorem CategoryTheory.Iso.toAlgEquiv_symm_apply {R : Type u} [CommRing R] {X Y : AlgCat R} (i : X ≅ Y) (a : ↑Y) : i.toAlgEquiv.symm a = (ConcreteCategory.hom i.inv) a

@[simp]

theorem CategoryTheory.Iso.toAlgEquiv_apply {R : Type u} [CommRing R] {X Y : AlgCat R} (i : X ≅ Y) (a : ↑X) : i.toAlgEquiv a = (ConcreteCategory.hom i.hom) a

def algEquivIsoAlgebraIso {R : Type u} [CommRing R] {X Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebra R Y] : (X ≃ₐ[R] Y) ≅ AlgCat.of R X ≅ AlgCat.of R Y

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

@[simp]

theorem algEquivIsoAlgebraIso_inv {R : Type u} [CommRing R] {X Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebra R Y] (i : AlgCat.of R X ≅ AlgCat.of R Y) : algEquivIsoAlgebraIso.inv i = i.toAlgEquiv

@[simp]

theorem algEquivIsoAlgebraIso_hom {R : Type u} [CommRing R] {X Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebra R Y] (e : X ≃ₐ[R] Y) : algEquivIsoAlgebraIso.hom e = e.toAlgebraIso

instance AlgCat.forget_reflects_isos {R : Type u} [CommRing R] : (CategoryTheory.forget (AlgCat R)).ReflectsIsomorphisms