Module

GeneratorRelationHOne.lean

Nyll.EtaleFundamentalGroups.Purity.Local.GeneratorRelationHOne

4 declarations indexed from sourceView source ↗

Module documentation

The first relation module of a finite list of generators

For elements f i : R, this file packages the elementary degree-one Koszul relation module

{x | f i • x j = f j • x i} / {i ↦ f i • m}.

Its key property is that it is annihilated by the ideal generated by the f i. This is the finite-generator calculation used when clearing denominators in formal gluing.

Imports1

Mathlib.Algebra.Module.Torsion.Basic

Imported by1

Nyll.EtaleFundamentalGroups.Purity.Local.All

def

generatorRelationCycles

L34 ↗

EtaleFundamentalGroups.generatorRelationCycles

Documentation

Tuples satisfying the degree-one Koszul relations for f.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u v w
variable {R : Type u} [CommRing R]
variable {ι : Type v}
variable (f : ι → R)
variable (M : Type w) [AddCommGroup M] [Module R M]

Lean source · full declaration

def generatorRelationCycles : Submodule R (ι → M) where
  carrier := {x | ∀ i j, f i • x j = f j • x i}
  zero_mem' := by simp
  add_mem' := by
    intro x y hx hy i j
    simp only [Pi.add_apply, smul_add, hx i j, hy i j]
  smul_mem' := by
    intro r x hx i j
    calc
      f i • (r • x j) = r • (f i • x j) := smul_comm _ _ _
      _ = r • (f j • x i) := congrArg (r • ·) (hx i j)
      _ = f j • (r • x i) := (smul_comm _ _ _).symm

def

generatorRelationBoundary

L49 ↗

EtaleFundamentalGroups.generatorRelationBoundary

Documentation

The diagonal boundary m ↦ (f i • m)ᵢ, with codomain restricted to the relation cycles.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u v w
variable {R : Type u} [CommRing R]
variable {ι : Type v}
variable (f : ι → R)
variable (M : Type w) [AddCommGroup M] [Module R M]

Lean source · full declaration

def generatorRelationBoundary :
    M →ₗ[R] generatorRelationCycles f M where
  toFun m := ⟨fun i ↦ f i • m, by
    intro i j
    rw [← mul_smul, mul_comm, mul_smul]⟩
  map_add' x y := by
    ext i
    simp
  map_smul' r x := by
    ext i
    exact smul_comm _ _ _

abbrev