Adjunctions in CommRingCat

Main results

• CommRingCat.adj: σ ↦ ℤ[σ] is left adjoint to the forgetful functor CommRingCat ⥤ Type.
• CommRingCat.coyonedaAdj: Fun(-, R) is left adjoint to Hom_{CRing}(R, -).
• CommRingCat.monoidAlgebraAdj: G ↦ R[G] as CommGrp ⥤ R-Alg is left adjoint to S ↦ Sˣ.
• CommRingCat.unitsAdj: G ↦ ℤ[G] is left adjoint to S ↦ Sˣ.

def CommRingCat.free : CategoryTheory.Functor (Type u) CommRingCat

The free functor Type u ⥤ CommRingCat sending a type X to the multivariable (commutative) polynomials with variables x : X.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommRingCat.free_obj_coe {α : Type u} : ↑(free.obj α) = MvPolynomial α ℤ

theorem CommRingCat.free_map_coe {α β : Type u} {f : α → β} : ⇑(CategoryTheory.ConcreteCategory.hom (free.map f)) = ⇑(MvPolynomial.rename f)

def CommRingCat.adj : free ⊣ CategoryTheory.forget CommRingCat

The free-forgetful adjunction for commutative rings.

Equations

• One or more equations did not get rendered due to their size.

instance CommRingCat.instIsRightAdjointForget : (CategoryTheory.forget CommRingCat).IsRightAdjoint

def CommRingCat.coyoneda : CategoryTheory.Functor Type vᵒᵖ (CategoryTheory.Functor CommRingCat CommRingCat)

Fun(-, -) as a functor Type vᵒᵖ ⥤ CommRingCat ⥤ CommRingCat.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommRingCat.coyoneda_map_app {m n : Type vᵒᵖ} (f : m ⟶ n) (R : CommRingCat) : (coyoneda.map f).app R = ofHom (Pi.ringHom fun (x : Opposite.unop n) => Pi.evalRingHom (fun (a : Opposite.unop m) => ↑R) (f.unop x))

@[simp]

theorem CommRingCat.coyoneda_obj_obj_carrier (n : Type vᵒᵖ) (R : CommRingCat) : ↑((coyoneda.obj n).obj R) = (Opposite.unop n → ↑R)

@[simp]

theorem CommRingCat.coyoneda_obj_map (n : Type vᵒᵖ) {R S : CommRingCat} (φ : R ⟶ S) : (coyoneda.obj n).map φ = ofHom (Pi.ringHom fun (x : Opposite.unop n) => (Hom.hom φ).comp (Pi.evalRingHom (fun (a : Opposite.unop n) => ↑R) x))

def CommRingCat.coyonedaAdj (R : CommRingCat) : (coyoneda.flip.obj R).rightOp ⊣ CategoryTheory.yoneda.obj R

The adjunction Hom_{CRing}(Fun(n, R), S) ≃ Fun(n, Hom_{CRing}(R, S)).

Equations

• One or more equations did not get rendered due to their size.

instance CommRingCat.instIsRightAdjointOppositeObjFunctorTypeYoneda (R : CommRingCat) : (CategoryTheory.yoneda.obj R).IsRightAdjoint

def CommRingCat.coyonedaUnique {n : Type v} [Unique n] : coyoneda.obj (Opposite.op n) ≅ CategoryTheory.Functor.id CommRingCat

If n is a singleton, Hom(n, -) is the identity in CommRingCat.

Equations

• CommRingCat.coyonedaUnique = CategoryTheory.NatIso.ofComponents (fun (X : CommRingCat) => (RingEquiv.piUnique fun (i : Opposite.unop (Opposite.op n)) => ↑X).toCommRingCatIso) ⋯

@[simp]

theorem CommRingCat.coyonedaUnique_inv_app_hom_apply {n : Type v} [Unique n] (X : CommRingCat) (a✝ : ↑X) (a✝¹ : Opposite.unop (Opposite.op n)) : (Hom.hom (coyonedaUnique.inv.app X)) a✝ a✝¹ = a✝

@[simp]

theorem CommRingCat.coyonedaUnique_hom_app_hom_apply {n : Type v} [Unique n] (X : CommRingCat) (a✝ : Opposite.unop (Opposite.op n) → ↑X) : (Hom.hom (coyonedaUnique.hom.app X)) a✝ = a✝ default

def CommRingCat.monoidAlgebra (R : CommRingCat) : CategoryTheory.Functor CommMonCat (CategoryTheory.Under R)

The monoid algebra functor CommGrp ⥤ R-Alg given by G ↦ R[G].

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommRingCat.monoidAlgebra_map (R : CommRingCat) {X✝ Y✝ : CommMonCat} (f : X✝ ⟶ Y✝) : R.monoidAlgebra.map f = CategoryTheory.Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯

@[simp]

theorem CommRingCat.monoidAlgebra_obj (R : CommRingCat) (G : CommMonCat) : R.monoidAlgebra.obj G = CategoryTheory.Under.mk (ofHom MonoidAlgebra.singleOneRingHom)

instance CommRingCat.instHasForget₂CommMonCat_1 : CategoryTheory.HasForget₂ CommRingCat CommMonCat

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommRingCat.instHasForget₂CommMonCat_1_forget₂_obj_coe (M : CommRingCat) : ↑(CategoryTheory.HasForget₂.forget₂.obj M) = ↑M

@[simp]

theorem CommRingCat.instHasForget₂CommMonCat_1_forget₂_map {X✝ Y✝ : CommRingCat} (f : X✝ ⟶ Y✝) : CategoryTheory.HasForget₂.forget₂.map f = CommMonCat.ofHom ↑(Hom.hom f)

def CommRingCat.monoidAlgebraAdj (R : CommRingCat) : R.monoidAlgebra ⊣ (CategoryTheory.Under.forget R).comp (CategoryTheory.forget₂ CommRingCat CommMonCat)

The adjunction G ↦ R[G] and S ↦ S between CommGrp and R-Alg.

Equations

• One or more equations did not get rendered due to their size.

def CommRingCat.forget₂Adj {R : CommRingCat} (hR : CategoryTheory.Limits.IsInitial R) : R.monoidAlgebra.comp (CategoryTheory.Under.forget R) ⊣ CategoryTheory.forget₂ CommRingCat CommMonCat

The adjunction G ↦ ℤ[G] and R ↦ Rˣ between CommGrp and CommRing.

Equations

• CommRingCat.forget₂Adj hR = R.monoidAlgebraAdj.comp (CategoryTheory.Under.equivalenceOfIsInitial hR).toAdjunction

instance CommRingCat.instIsLeftAdjointCommMonCatUnderMonoidAlgebra (R : CommRingCat) : R.monoidAlgebra.IsLeftAdjoint

instance CommRingCat.instIsRightAdjointCommMonCatForget₂ : (CategoryTheory.forget₂ CommRingCat CommMonCat).IsRightAdjoint