Module

BoundaryModule.lean

Nyll.AnabelianGeometry.CuspidalInertia.BoundaryModule

7 declarations indexed from sourceView source ↗

Module documentation

The reduced boundary module

The boundary permutation module is taken modulo its diagonal relation. With at least two labels, each coordinate injects into the quotient. With three distinct labels, two coordinate lines have zero intersection. These are integral statements over any commutative ring; no division by the number of boundary points is used.

Imports3

Mathlib.LinearAlgebra.Quotient.Defs
Mathlib.Algebra.Module.Pi
Mathlib.Algebra.BigOperators.Pi

Imported by3

def

boundaryDiagonal

L28 ↗

AnabelianGeometry.CuspidalInertia.boundaryDiagonal

Documentation

The diagonal submodule of constant functions.

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 boundaryDiagonal : Submodule R (ι → R) where
  carrier := {f | ∃ a : R, ∀ i, f i = a}
  zero_mem' := ⟨0, fun _ => rfl⟩
  add_mem' := by
    rintro f g ⟨a, ha⟩ ⟨b, hb⟩
    refine ⟨a + b, ?_⟩
    intro i
    change f i + g i = a + b
    rw [ha i, hb i]
  smul_mem' := by
    rintro a f ⟨b, hb⟩
    refine ⟨a * b, ?_⟩
    intro i
    change a * f i = a * b
    rw [hb i]

abbrev

BoundaryModule

L45 ↗

AnabelianGeometry.CuspidalInertia.BoundaryModule

Documentation

The permutation module modulo 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

abbrev BoundaryModule

def

boundaryClass

L50 ↗

AnabelianGeometry.CuspidalInertia.boundaryClass

Documentation

A weighted boundary coordinate in the reduced module.

Source context 4 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)
variable {R ι} [DecidableEq ι]

Lean source · statement

def boundaryClass (i : ι) (a : R) : BoundaryModule R ι

theorem

boundaryClass_injective

L54 ↗

AnabelianGeometry.CuspidalInertia.boundaryClass_injective

Documentation

One boundary coordinate injects whenever a second label is available.

Source context 4 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)
variable {R ι} [DecidableEq ι]

Lean source · statement

theorem boundaryClass_injective (i j : ι) (hji : j ≠ i) :
    Function.Injective (boundaryClass (R := R) i)

theorem

boundaryClass_eq_implies_coefficients_zero

L66 ↗

AnabelianGeometry.CuspidalInertia.boundaryClass_eq_implies_coefficients_zero

Documentation

Distinct boundary coordinate lines meet trivially if a third label exists.

Source context 4 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)
variable {R ι} [DecidableEq ι]

Lean source · statement

theorem boundaryClass_eq_implies_coefficients_zero
    (i j k : ι) (hij : i ≠ j) (hki : k ≠ i) (hkj : k ≠ j)
    {a b : R} (h : boundaryClass i a = boundaryClass j b) : a = 0 ∧ b = 0

theorem

sum_boundaryClass

L83 ↗

AnabelianGeometry.CuspidalInertia.sum_boundaryClass

Documentation

Summing weighted boundary coordinates is the quotient map on the full permutation module.

Source context 4 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)
variable {R ι} [DecidableEq ι]

Lean source · statement

theorem sum_boundaryClass [Fintype ι] (a : ι → R) :
    (∑ i : ι, boundaryClass i (a i)) =
      (Submodule.Quotient.mk a : BoundaryModule R ι)

theorem

sum_boundaryClass_eq_zero_iff

L101 ↗

AnabelianGeometry.CuspidalInertia.sum_boundaryClass_eq_zero_iff

Documentation

The diagonal is the entire relation module among boundary coordinates.

Source context 4 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)
variable {R ι} [DecidableEq ι]

Lean source · statement

theorem sum_boundaryClass_eq_zero_iff [Fintype ι] (a : ι → R) :
    (∑ i : ι, boundaryClass i (a i)) = 0 ↔ ∃ c : R, ∀ i, a i = c

Module documentation

The reduced boundary module

Declarations

boundaryDiagonal

BoundaryModule

boundaryClass

boundaryClass_injective

boundaryClass_eq_implies_coefficients_zero

sum_boundaryClass

sum_boundaryClass_eq_zero_iff