Registry · Definition I.D48 tau-effective formalized

I.D48 — Tau-Holomorphic Map

A tau-holomorphic map bundles a HolFun with source and target object indices in tau-Idx. Provides the morphism data for the earned category Cat_tau (Part XIII).

Book I Part 13 Ch. 50

Dependency Graph

Depends on (1)

I.D47

Lean Formalization

Module: TauLib.BookI.Holomorphy.TauHolomorphic

Symbol: Tau.Holomorphy.HolMap