DivisorialPointedQuotientTriviality.lean
Nyll.EtaleFundamentalGroups.Inertia.DivisorialPointedQuotientTriviality
0 declarations indexed from sourceView source ↗
Module documentation
Triviality from pointed divisorial quotients
The actual pointed finite-cover quotient recovers normalization-prime ideal inertia after the canonical deck-group and base-point conjugation transports. Consequently, coprimality of its finite image with every prime forces ideal inertia to be trivial.
The declarations live in DivisorialPointedQuotientEndpoint so that the comparison, range transport, and triviality proofs share one local instance graph. This module is the narrow compatibility facade for that API.
This module has no indexed declarations. Its imports and full source are available here.