The coefficient maps are the native maps stored by the commutative algebra objects. The categorical morphism is constructed only after its actual RingHom coefficient square has been proved. No new algebra action is used.
The coefficient map of the actual native commutative algebra object.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable {A : Type u} [CommRing A]def commAlgCoefficientMap (R : CommAlgCat.{v} A) : A →+* RThe computed coefficient map is precisely the stored native action.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable {A : Type u} [CommRing A]theorem commAlgCoefficientMap_eq_algebraMap (R : CommAlgCat.{v} A) :
commAlgCoefficientMap R = algebraMap A RThe same native object in the category of algebras.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable {A : Type u} [CommRing A]def commAlgToAlgCat (R : CommAlgCat.{v} A) : AlgCat.{v} AConstruct the native categorical morphism from the actual ring map and its proved square with the stored coefficient maps.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable {A : Type u} [CommRing A]def commAlgRingHomToAlgCatHom (R S : CommAlgCat.{v} A) (f : R →+* S)
(h : f.comp (commAlgCoefficientMap R) = commAlgCoefficientMap S) :
AlgCat.Hom (commAlgToAlgCat R) (commAlgToAlgCat S)The categorical construction retains the given actual RingHom.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable {A : Type u} [CommRing A]theorem commAlgRingHomToAlgCatHom_toRingHom
(R S : CommAlgCat.{v} A) (f : R →+* S)
(h : f.comp (commAlgCoefficientMap R) = commAlgCoefficientMap S) :
(commAlgRingHomToAlgCatHom R S f h).hom.toRingHom = f