В предыдущем посте мы обсудили, как мы можем сформулировать определение общей законной оптики, и мы доказали, что законные линзы - это в точности линзы с постоянным дополнением.

В этом посте мы вернемся к представленным там идеям в более категоричной форме, но сосредоточимся, в частности, на линзах.

В этом посте мы представим серию результатов, которые были получены на третьем Statebox Summit при сотрудничестве участников, из которых следует упомянуть Жюля Хеджеса, Дэвида Спивака, Брендана Фонга. , Кристине Василакопулу, Элиане Лорч , Андре Книспелю и Стефано Гогиозо за активное участие в дискуссии.

Категория линз

Начнем с определения категории линз. Объектами нашей категории будут пары наборов (S, T), морфизмы между (S, T) и (A, B) будут линзами типа Lens S T A B, которые описываются парами функций.

g : S → A
p : S → B → T

Композиция из двух морфизмов, то есть двух линз, (g, p) : (S, T) → (A, B) и (h, q) : (A, B) → (C, D), представляет собой новую линзу (g', p') : Lens S T C D, определяемую функциями

g' : S → C
g' = g ; h
p' : S → D → T
p' s d = p s (q (g s) d)

где p' может быть представлен следующей диаграммой

где ∙ : S → S × S - операция copy.

Для любого объекта нашей категории, который является парой (S, T), морфизм идентичности на нем - это линза (gᵢ, pᵢ) : (S, T) → (S, T), определяемая

gᵢ : S → S
gᵢ s = s
pᵢ : S → T → T
pᵢ s t = t

Можно проверить, что приведенные выше определения удовлетворяют аксиомам категории.

Связанные линзы

Учитывая общий объектив L := (g, p) : (S, T) → (A, B), мы увидели в этом посте, что можем определить набор

M = { m ∈ B → T | ∃ s : S . m = p s }

что оказывается действительно полезным в доказательстве того, что законные линзы - это в точности линзы с постоянным дополнением. Фактически, этот набор позволяет нам определить две новые линзы, связанные с линзой L.

Во-первых, мы можем определить L* : (S, T) → (A × M, B × M) следующим образом:

g*: S → A × M
g* s = (g s, p s)
p* : S → B × M → T
p* s (b, m) = m b

Кроме того, мы также можем определить L^ : (B × M, A × M) → (T, S) как

g^ : B × M → T
g^ (b, m) = m b
p^ : B × M → S → A × M
p^ (b, m) s = (g s, p s)

Обратите внимание, как ^ (произносится «шляпа») производит обмен между A и B и между S и T. В их общей форме L* и L^ не могут быть составлены. Однако, если мы ограничимся простыми линзами, они будут такими!

Итак, с этими двумя новыми объективами естественно возникают некоторые вопросы.

  • Когда в простом случае линз L* и L^ противоположны друг другу?
  • Когда в простом футляре объектива разрешены L* и L^?
  • В общем случае, если мы рассматриваем π : (A × M, B × M) → (A, B) как линзу, определяемую
gπ : A × M → A
gπ (a, m) = a
pπ : A × M → B → B × M 
pπ (a, m) b = (b, m)

всегда ли правда, что L = L* ; π?

Являются ли L* и L^ перевернутыми?

Рассмотрим сначала состав L* ; L^. В этом случае мы имеем

g*^ : S → S
g*^ s = p s (g s) = s -- by getput
p*^ : S → S → S
p*^ s₁ s₂ = p s₂ (g s₂) = s₂ -- by getput

Следовательно, L^ ; L^ = id на (S, S) тогда и только тогда, когда getput выполняется для L.

С другой стороны, рассмотрите L^ ; L*. Мы получаем

g^* : A × M → A × M
g^* (a, m) = (g (m a), p (m a))
p^* : A × M → A × M → A × M
p^* (a₁, m₁) (a₂, m₂) = (g (m₂ a₂), p (m₂ a₂))

Помните, что по определению M мы имеем, что любой m ∈ M имеет форму p s для некоторого s ∈ S. Отсюда получаем

g^* : A × M → A × M
g^* (a, p s) = (g (p s a), p (p s a))
             = (a, p s) -- by putget and putput
p^* : A × M → A × M → A × M
p^* (a₁, p s₁) (a₂, p s₂) = (g (p s₂ a₂), p (p s₂ a₂))
                          = (a₂, p s₂) -- by putget and putput

Затем мы получаем это L^ ; L* = id на (M × A) всякий раз, когда L удовлетворяет putget и putput.

В заключение мы говорим, что L* и L^ инвертируют друг друга тогда и только тогда, когда L является законной линзой.

Законны ли L * и L ^?

В этом разделе мы проверим, являются ли L* и L^ допустимыми линзами в простом случае, и какие условия нам нужно принять на L, чтобы они удовлетворяли законам линз.

Начнем с L*

getput

p* s (g* s) = p s (g s) = s -- by getput

путгет

g* (p* s₁ (a, p s₂)) = g* (p s₂ a)
                     = (g (p s₂ a), p (p s₂ a))
                     = (a, p s₂) -- by putget and putput

putput

p* (p* s (a₁, m₁)) (a₂, m₂) = p* (m₁ a₁) (a₂, m₂)
                            = m₂ a₂
                            = p* s (a₂, m₂) -- always holds

Следовательно, L* всегда удовлетворяет putput, удовлетворяет getput, если L удовлетворяет getput, и удовлетворяет putget, если L удовлетворяет putget и putput. Следовательно, L* является законным тогда и только тогда, когда L является законным.

Давайте теперь посмотрим на L^.

getput

p^ (a, p s) (g^ (a, p s)) = p^ (a, p s) (p s a)
                          = (g (p s a), p (p s a))
                          = (a, p s) -- by putget and putput

путать

g^ (p^ (a, m) s) = g^ (g s, p s)
                 = p s (g s)
                 = s -- by getput

putput

p^ (p^ (a, m) s₁) s₂ = p^ (g s₁, p s₁) s₂
                     = (g s₂, p s₂)
                     = p^ (a, m) s₂ -- always

Следовательно, L^ всегда удовлетворяет putput, и он удовлетворяет getput, если L удовлетворяет putget и putput, и удовлетворяет putget, если L удовлетворяет getput. Таким образом, L^ является законным тогда и только тогда, когда L является законным.

Разложение L

Остается один вопрос: держится ли L = L* ; π. Нетрудно убедиться, что так происходит всегда; фактически, если мы вычислим компоненты g° и p° для составной линзы, мы получим

g° : S → A
g° s = gπ (g* s) = gπ (g s, p s) = g s
p° : S → B → T
p° s b = p* (s, pπ (g* s, b))
       = p* (s, pπ ((g s, p s), b))
       = p* (s, (b, p s)) = p s b

В заключение, мы всегда можем разложить L на L* ; π, где π всегда законно.

Заключение

В этом посте мы более подробно исследовали роль M, а также линзы L* и L^, которые были созданы на его основе. Мы видели, что L* и L^ строго связаны с L, и что они удовлетворяют законам линз, только если L удовлетворяет другим законам линз.

Объединив три результата, представленных выше, мы также можем получить более формальное доказательство того, что простая линза является законной тогда и только тогда, когда она изоморфна линзе с постоянным дополнением.

Некоторые дополнительные вопросы, которые мы могли бы рассмотреть

  • Что такое M для L* и L^?
  • Как L**, L*^, L^* и L^^ связаны с L, L* и L^?
  • Есть ли связь между M, являющимся одноэлементным набором, и изоморфизмами в категории линз (легко доказать, что M = {*} означает, что L удовлетворяет putput)?
  • Можно ли обобщить свойства, сформулированные для простого случая, на общий случай?