FoxDifferential/Discrete/KernelBoundary.lean
1import FoxDifferential.Discrete.KernelBoundary.IdentityAugmentation
2import FoxDifferential.Discrete.KernelBoundary.Basic
3import FoxDifferential.Discrete.KernelBoundary.Homology
4import FoxDifferential.Discrete.KernelBoundary.Quotient
5import FoxDifferential.Discrete.KernelBoundary.MagnusKernel
7/-
8PUBLIC_PAGE_SNAPSHOT
9generated_at: 2026-05-27T09:47:29+09:00
10lean_source: lean4/FoxDifferential/Discrete/KernelBoundary.lean
11translation_root: data/translation
12purpose: identifies the local data snapshot used to build pages/
13placement: after imports, never before imports
14-/
15/-!
16# Kernel-boundary algebra for Fox differential modules
18This module collects the kernel-abelianization boundary, the identity differential module,
19the kernel-augmentation homology comparison, the quotient bridge, and the Magnus-kernel theorem.
20It is part of the general discrete Fox layer and is used by Crowell exact sequences and MPC.
21-/