Module

BoundaryRetraction.lean

Nyll.AnabelianGeometry.CuspidalInertia.BoundaryRetraction

4 declarations indexed from sourceView source ↗

Module documentation

Integral retractions of boundary coordinates

Differences of coordinate evaluations vanish on the diagonal relation and therefore descend to the reduced boundary module. They recover a boundary coefficient integrally, without division by the number of punctures.

Imports3

Nyll.AnabelianGeometry.CuspidalInertia.BoundaryModule
Mathlib.LinearAlgebra.Quotient.Basic
Mathlib.Tactic.Ring

Imported by2

def

boundaryEvaluationDifference

L26 ↗

AnabelianGeometry.CuspidalInertia.boundaryEvaluationDifference

Documentation

Difference of two evaluations on the boundary permutation 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}

Lean source · full declaration

def boundaryEvaluationDifference (i j : ι) : (ι → R) →ₗ[R] R where
  toFun f := f i - f j
  map_add' f g := by
    change (f i + g i) - (f j + g j) = (f i - f j) + (g i - g j)
    ring
  map_smul' a f := by
    change a * f i - a * f j = a * (f i - f j)
    exact (mul_sub a (f i) (f j)).symm

def

boundaryDifference

L36 ↗

AnabelianGeometry.CuspidalInertia.boundaryDifference

Documentation

Difference of evaluations descends through the diagonal relation.

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}

Lean source · statement

def boundaryDifference (i j : ι) : BoundaryModule R ι →ₗ[R] R

theorem

boundaryDifference_mk

L43 ↗

AnabelianGeometry.CuspidalInertia.boundaryDifference_mk

Documentation

Evaluating a quotient representative gives its coordinate difference.

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}

Lean source · statement

theorem boundaryDifference_mk (i j : ι) (f : ι → R) :
    boundaryDifference (R := R) i j (Submodule.Quotient.mk f : BoundaryModule R ι) =
      f i - f j

theorem

boundaryDifference_boundaryClass

L49 ↗

AnabelianGeometry.CuspidalInertia.boundaryDifference_boundaryClass

Documentation

The descended coordinate difference is an integral left inverse to a boundary coordinate whenever the other label is distinct.

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}

Lean source · statement

theorem boundaryDifference_boundaryClass [DecidableEq ι]
    (i j : ι) (hji : j ≠ i) (a : R) :
    boundaryDifference (R := R) i j (boundaryClass i a : BoundaryModule R ι) = a

Module documentation

Integral retractions of boundary coordinates

Declarations

boundaryEvaluationDifference

boundaryDifference

boundaryDifference_mk

boundaryDifference_boundaryClass