Module

RootsOfUnityDegreeEquiv.lean

Nyll.EtaleFundamentalGroups.Inertia.RootsOfUnityDegreeEquiv

2 declarations indexed from sourceView source ↗

Module documentation

Transport of root groups along equality of their degrees

The transport keeps the actual unit. Its scalar computation, inverse, and homomorphism structure are built together, before any field tower appears.

Imports1

Mathlib.RingTheory.RootsOfUnity.Basic

Imported by2

def

rootsOfUnityDegreeEquiv

L21 ↗

EtaleFundamentalGroups.Inertia.rootsOfUnityDegreeEquiv

Documentation

Equality of degrees identifies their root groups without changing units.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · full declaration

def rootsOfUnityDegreeEquiv (R : Type u) [CommMonoid R]
    {m n : ℕ} (h : m = n) : rootsOfUnity m R ≃* rootsOfUnity n R where
  toFun ζ := ⟨ζ.val, h ▸ ζ.property⟩
  invFun ζ := ⟨ζ.val, h.symm ▸ ζ.property⟩
  left_inv _ := rfl
  right_inv _ := rfl
  map_mul' _ _ := rfl

theorem

rootsOfUnityDegreeEquiv_val

L30 ↗

EtaleFundamentalGroups.Inertia.rootsOfUnityDegreeEquiv_val