Module

BoundaryPermutation.lean

Nyll.AnabelianGeometry.CuspidalInertia.BoundaryPermutation

4 declarations indexed from sourceView source ↗

Module documentation

Permutations of the reduced boundary module

Permuting boundary labels preserves the diagonal relation and induces a linear equivalence on the reduced boundary module. The equivalence sends each boundary coordinate to its permuted coordinate.

Imports2

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

Imported by1

Nyll.AnabelianGeometry.CuspidalInertia.All

def

boundaryReindex

AnabelianGeometry.CuspidalInertia.boundaryReindex

Documentation

Reindex the full 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 boundaryReindex (e : ι ≃ ι) : (ι → R) →ₗ[R] (ι → R) where
  toFun f j := f (e.symm j)
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

def

boundaryPermutation

AnabelianGeometry.CuspidalInertia.boundaryPermutation

Documentation

The induced map on the quotient by 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 boundaryPermutation (e : ι ≃ ι) : BoundaryModule R ι →ₗ[R] BoundaryModule R ι

def

boundaryPermutationEquiv

AnabelianGeometry.CuspidalInertia.boundaryPermutationEquiv

Documentation

A permutation acts invertibly on the reduced boundary 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 boundaryPermutationEquiv (e : ι ≃ ι) :
    BoundaryModule R ι ≃ₗ[R] BoundaryModule R ι where
  toLinearMap := boundaryPermutation (R := R) e
  invFun := boundaryPermutation (R := R) e.symm
  left_inv x := by
    refine Quotient.inductionOn x ?_
    intro f
    change (Submodule.Quotient.mk (fun j => f (e.symm (e j))) : BoundaryModule R ι) =
      Submodule.Quotient.mk f
    congr 1
    funext j
    rw [e.symm_apply_apply]
  right_inv x := by
    refine Quotient.inductionOn x ?_
    intro f
    change (Submodule.Quotient.mk (fun j => f (e (e.symm j))) : BoundaryModule R ι) =
      Submodule.Quotient.mk f
    congr 1
    funext j
    rw [e.apply_symm_apply]

theorem

boundaryPermutation_boundaryClass

AnabelianGeometry.CuspidalInertia.boundaryPermutation_boundaryClass

Documentation

Boundary coordinates are permuted with their labels, with coefficients unchanged.

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 boundaryPermutation_boundaryClass [DecidableEq ι]
    (e : ι ≃ ι) (i : ι) (a : R) :
    boundaryPermutation (R := R) e (boundaryClass i a) = boundaryClass (e i) a