NYLL
Module

NormalizationAutomorphismGroupMap.lean

Nyll.SchemeTheory.Normalization.NormalizationAutomorphismGroupMap
2 declarations indexed from sourceView source ↗

Module documentation

Normalization on automorphism group objects

Defines the coefficient automorphism group as a group object and the induced group morphism obtained by restriction to the normalization.

Imports5
Imported by6

Declarations

def

commAlgAutomorphismGroup

L27 ↗
SchemeTheory.commAlgAutomorphismGroup
Documentation

The native group of the original coefficient automorphisms.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v
Lean source · statement
def commAlgAutomorphismGroup (A : Type u) [CommRing A] (C : CommAlgCat.{v} A) : GrpCat.{v}
def

normalizationAutomorphismGroupMap

L31 ↗
SchemeTheory.normalizationAutomorphismGroupMap
Documentation

Actual normalization functoriality on coefficient automorphism groups.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v
Lean source · full declaration
def normalizationAutomorphismGroupMap (A : Type u) [CommRing A] (C : CommAlgCat.{v} A) :
    GrpCat.Hom (commAlgAutomorphismGroup A C)
      (commAlgAutomorphismGroup A (normalizationCommAlgCat A C)) where
  hom' := integralClosureAutHom A C

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.