The sheaf of units

This file constructs the sheaf of units of a sheaf of commutative rings. We regard the multiplicative group of units additively, so that the result takes values in AddCommGrpCat and can be used with kernels and cokernels in the abelian category of sheaves of abelian groups.

The construction is pointwise: the units functor is a right adjoint and therefore preserves the limits in the sheaf condition. Thus a sheaf of commutative rings F gives a sheaf whose sections over U are Additive (F(U)ˣ).

The sections and the restriction maps of the resulting sheaf are computed by additiveUnitsFunctor_obj_obj and additiveUnitsFunctor_obj_map_apply.

This is the categorical input for the Cartier-divisor sheaf 𝒦_X^× / 𝒪_X^× in TauCeti/AlgebraicGeometry/CartierDivisor/Basic.lean. No formalization is vendored; the construction composes Mathlib's CommMonCat.units, the multiplicative-to-additive equivalence, and CategoryTheory.sheafCompose.

@[reducible, inline]

abbrev CommRingCat.additiveUnits : CategoryTheory.Functor CommRingCat AddCommGrpCat

The functor from commutative rings to their groups of units, written additively.

Equations

• CommRingCat.additiveUnits = (CategoryTheory.forget₂ CommRingCat CommMonCat).comp (CommMonCat.units.comp commGroupAddCommGroupEquivalence.functor)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Sheaf.additiveUnitsFunctor {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : Functor (Sheaf J CommRingCat) (Sheaf J AddCommGrpCat)

Taking the units of a sheaf of commutative rings, written additively.

Equations

• CategoryTheory.Sheaf.additiveUnitsFunctor J = CategoryTheory.sheafCompose J CommRingCat.additiveUnits

@[simp]

theorem CategoryTheory.Sheaf.additiveUnitsFunctor_obj_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (F : Sheaf J CommRingCat) (U : Cᵒᵖ) : ((additiveUnitsFunctor J).obj F).obj.obj U = ↧(Additive (↑(F.obj.obj U))ˣ)

The sections of the additive units sheaf are the units of the original ring of sections.

@[simp]

theorem CategoryTheory.Sheaf.additiveUnitsFunctor_map_app_apply {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {F G : Sheaf J CommRingCat} (f : F ⟶ G) (U : Cᵒᵖ) (x : Additive (↑(F.obj.obj U))ˣ) : (AddCommGrpCat.Hom.hom (((additiveUnitsFunctor J).map f).hom.app U)) x = Additive.ofMul ((Units.map ↑(CommRingCat.Hom.hom (f.hom.app U))) (Additive.toMul x))

A morphism of additive units sheaves acts by applying the original ring morphism to a unit.

@[simp]

theorem CategoryTheory.Sheaf.additiveUnitsFunctor_obj_map_apply {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (F : Sheaf J CommRingCat) {U V : Cᵒᵖ} (i : U ⟶ V) (x : Additive (↑(F.obj.obj U))ˣ) : (AddCommGrpCat.Hom.hom (((additiveUnitsFunctor J).obj F).obj.map i)) x = Additive.ofMul ((Units.map ↑(CommRingCat.Hom.hom (F.obj.map i))) (Additive.toMul x))

Restricting a section of the additive units sheaf applies the restriction map of the underlying sheaf of rings to the underlying unit.