ModuleBoundaryCoordinates.lean
Nyll.AnabelianGeometry.CuspidalInertia.BoundaryCoordinates
4 declarations indexed from sourceView source ↗ Module documentation
Free coordinates for the reduced boundary module
Choosing one boundary label identifies the module modulo its diagonal with functions on all remaining labels. This gives an integral coordinate system; in particular, no inversion of the number of boundary points is needed.
Declarations
AnabelianGeometry.CuspidalInertia.boundaryCoordinates
DocumentationCoordinates relative to one distinguished boundary label.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.CuspidalInertia
universe u v
variable {R : Type u} [CommRing R] {ι : Type v}
AnabelianGeometry.CuspidalInertia.boundaryCoordinates_injective
DocumentationThe relative coordinates separate all classes modulo the diagonal.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.CuspidalInertia
universe u v
variable {R : Type u} [CommRing R] {ι : Type v}
AnabelianGeometry.CuspidalInertia.boundaryCoordinates_surjective
DocumentationEvery tuple of relative boundary coordinates has a representative.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.CuspidalInertia
universe u v
variable {R : Type u} [CommRing R] {ι : Type v}
AnabelianGeometry.CuspidalInertia.boundaryCoordinatesEquiv
DocumentationAn integral coordinate equivalence for the boundary relation module.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.CuspidalInertia
universe u v
variable {R : Type u} [CommRing R] {ι : Type v}