nLab delta lens

Redirected from "delta lenses".
Contents

Contents

Idea

A delta lens (or d-lens) is a functor with additional structure specifying a suitable choice of lifts. Delta lenses can be understood in a number of ways:

Definition

A delta lens (f,φ):AB(f, \varphi) : A \to B from a category AA to a category BB consists of a functor f:ABf : A \to B together with a lifting operation sending each pair (aA,u:fabB)(a \in A, u : f a \to b \in B) to a morphism φ(a,u):aa\varphi(a, u) : a \to a' in AA, where a=cod(φ(a,u))a' = cod(\varphi(a, u)), such that

  • φ\varphi defines a choice of lifts: fφ(a,u)=uf \varphi(a, u) = u,

  • φ\varphi preserves identity morphisms: φ(a,1 fa)=1 a\varphi(a, 1_{f a}) = 1_{a},

  • φ\varphi preserves composition: φ(a,vu)=φ(a,v)φ(a,u)\varphi(a, v \circ u) = \varphi(a', v) \circ \varphi(a, u) where a=cod(φ(a,u))a' = cod(\varphi(a, u)).

Properties

Proposition

A delta lens (f,φ):AB(f, \varphi) : A \to B is equivalent to a functor f:ABf \colon A \to B and a cofunctor φ:AB\varphi \colon A \nrightarrow B such that fa=φ 0af a = \varphi_{0} a for all objects aAa \in A, and fφ 1(aA,u:fabB)=uf \varphi_{1}(a \in A, u \colon fa \to b \in B) = u.

Examples

References

The notion of delta lens was first defined in computer science as a generalization of the classical lenses between sets:

  • Zinovy Diskin, Yingfei Xiong, Krzysztof Czarnecki, From State- to Delta-Based Bidirectional Model Transformations: the Asymmetric Case, Journal of Object Technology, 10, 2011 (doi:10.5381/jot.2011.10.1.a6)

The connection between delta lenses and split Grothendieck opfibrations was first explored in the paper:

The following paper details the connection between delta lenses and the classical lenses:

The characterisation of delta lenses in terms of functors and cofunctors first appeared in the paper:

The notion of delta lens between internal categories as well as the link between cofunctors, delta lenses, and split Grothendieck opfibrations is developed in the papers:

Last revised on August 11, 2023 at 10:40:04. See the history of this page for a list of all contributions to it.