Braided restriction of scalars

Restriction of scalars along a morphism of commutative rings is compatible with the symmetric braiding on module categories.

@[instance_reducible]

noncomputable instance TauCeti.ModuleCat.restrictScalarsLaxBraided {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : (ModuleCat.restrictScalars f).LaxBraided

Restriction of scalars between module categories preserves the symmetric braiding.

Equations

• TauCeti.ModuleCat.restrictScalarsLaxBraided f = { toLaxMonoidal := ModuleCat.instLaxMonoidalRestrictScalars f, braided := ⋯ }