Module

NativeAutomorphismRingMaps.lean

Nyll.SchemeTheory.Normalization.NativeAutomorphismRingMaps

3 declarations indexed from sourceView source ↗

Module documentation

Defines the underlying ring maps of coefficient and Galois automorphisms, together with the inclusion of the normalization into its ambient algebra.

Imports3

Imported by14

def

SchemeTheory.commAlgAutomorphismRingHom

Documentation

The individual actual coefficient automorphism as a ring map.

Source context 2 commands

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

namespace SchemeTheory
universe u v

Lean source · statement

def commAlgAutomorphismRingHom (A : Type u) [CommRing A] (C : CommAlgCat.{v} A)
    (g : commAlgAutomorphismGroup A C) : C →+* C

def

SchemeTheory.galoisAutomorphismRingHom

Documentation

The individual actual field automorphism as a ring map.

Source context 2 commands

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

namespace SchemeTheory
universe u v

Lean source · statement

def galoisAutomorphismRingHom (K : Type u) (L : Type v)
    [Field K] [Field L] [Algebra K L] (g : Gal(L/K)) : L →+* L

def

SchemeTheory.normalizationAmbientRingHom

Documentation

The native normalization coefficient inclusion into its ambient algebra.

Source context 2 commands

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

namespace SchemeTheory
universe u v

Lean source · statement

def normalizationAmbientRingHom (A : Type u) [CommRing A] (C : CommAlgCat.{v} A) :
    normalizationCommAlgCat A C →+* C