Yamaguchi Lean 4 Library
FoxDifferential.Completed.Continuous.Universal
FoxDifferential/Completed/Continuous/Universal

FoxDifferential.Completed.Continuous.Universal

5 sections | 5 files | 438 declarations

Wrapper for the FoxDifferential.Completed.Continuous.Universal folder.

AugmentationQuotient

1 files | 207 declarations | 158 Theorem | 45 Definition | 4 Abbreviation
The algebraic product \(I(\ker \psi)I(G)\) inside the algebraic standard source augmentation ideal.

Basic

1 files | 30 declarations | 16 Theorem | 10 Definition | 4 Instance
The final topology on the completed universal differential module generated by the universal crossed differential \(G \to d_{\mathbb{Z}_C\llbracket H\rrbracket}G\). Unlike the f...

FiniteStage

1 files | 86 declarations | 58 Theorem | 16 Definition | 4 Abbreviation | 1 Structure | 7 Instance
A finite stage for the completed universal differential module. It consists of a finite source quotient \(G/V\), a coefficient-and-target stage \((\mathbb{Z}/n\mathbb{Z})[H/U]\)...

NaturalTopology

1 files | 104 declarations | 78 Theorem | 23 Definition | 3 Abbreviation
The additive finite-stage projection from the algebraic completed differential module.

System

1 files | 11 declarations | 5 Theorem | 3 Definition | 1 Abbreviation | 2 Instance
The inverse system of finite source, target, and coefficient stages of \(A_{\psi}(C)\).