18.2. The unbundled vs. bundled barrier.🔗

When working in algebraic geometry in mathlib, we often have to cross the unbundled vs. bundled barrier. To explain what we mean by this, consider the following example:

The composition of two ring homomorphisms can be expressed as:

example (R S T : Type) [CommRing R] [CommRing S]
    [CommRing T] (f : R →+* S) (g : S →+* T) :
    R →+* T :=
  RingHom.comp g f

or as:

example (R S T : CommRingCat) (f : R ⟶ S) (g : S ⟶ T) :
    R ⟶ T :=
  f ≫ g

The first approach is called unbundled and the second one bundled: In the first version, the CommRing structure on R is provided as a separate argument. It is unbundled from the type R. In the second version, the CommRing structure is bundled with the type in a term R of type CommRingCat.

Note that we have to write R →+* S in the first case to talk about a ring homomorphism f. This is because R S : Type. In the case of R S : CommRingCat, the types contain enough information to infer that R ⟶ S denotes a ring homomorphism.

Moreover, in the bundled version we can use the notation f ≫ g to denote composition of the ring homomorphisms f and g.

Most of the topology and commutative algebra library is written in the unbundled style. But to talk about the category of commutative rings or the category of topological spaces, this category needs a type of objects.

example : Type 1 := CommRingCat

To go between the unbundled and the bundled world, use CommRingCat.of and CommRingCat.ofHom. For example:

example (R S : Type) [CommRing R] [CommRing S]
    (f : R →+* S) :
    CommRingCat.of R ⟶ CommRingCat.of S :=
  CommRingCat.ofHom f

Conversely, a morphism in CommRingCat has an underlying ring homomorphism.

example (R S : CommRingCat) (f : R ⟶ S) : R →+* S := f.hom

We can still apply a morphism in CommRingCat to an element.

example (R S : CommRingCat) (f : R ⟶ S) (x : R) : S := f x

The type of commutative rings is endowed with a category structure.

open CategoryTheory -- required for category notation
example : Category CommRingCat := inferInstance

This allows us to write 𝟙 _ for the identity and _ ≫ _ for composition:

example (R S : CommRingCat) (f : R ⟶ S) : R ⟶ S :=
  𝟙 R ≫ f ≫ 𝟙 S