Module

AmbientNormalizationGroupMap.lean

Nyll.SchemeTheory.Normalization.AmbientNormalizationGroupMap

3 declarations indexed from sourceView source ↗

Module documentation

Ambient field automorphisms on normalizations

Constructs the action of ambient field automorphisms on the normalization by restriction of scalars and integral-closure functoriality. The induced ring maps commute with the inclusion into the ambient field.

Imports3

Imported by11

def

normalizationGaloisGroupMap

L32 ↗

SchemeTheory.normalizationGaloisGroupMap

Documentation

The original ambient field automorphisms act on its actual normalization.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open CategoryTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L] [Algebra A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L]

Lean source · full declaration

def normalizationGaloisGroupMap :
    GrpCat.Hom (galoisGroupObject K L)
      (commAlgAutomorphismGroup A (normalizationCommAlgCat A L)) where
  hom' := (normalizationAutomorphismGroupMap A (CommAlgCat.of A L)).hom'.comp
    (scalarRestrictionGroupMap A K (CommAlgCat.of A L)).hom'

def

normalizationGaloisRingHom

L39 ↗

SchemeTheory.normalizationGaloisRingHom

Documentation

The individual original normalization action as its actual ring map.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open CategoryTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L] [Algebra A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L]

Lean source · statement

def normalizationGaloisRingHom (σ : Gal(L/K)) :
    (normalizationCommAlgCat A L).carrier →+* (normalizationCommAlgCat A L).carrier

theorem

normalizationGaloisRingHom_commutes

L45 ↗

SchemeTheory.normalizationGaloisRingHom_commutes

Documentation

Normalization functoriality gives the actual ambient coefficient square.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open CategoryTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L] [Algebra A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L]

Lean source · statement

theorem normalizationGaloisRingHom_commutes (σ : Gal(L/K)) :
    (normalizationAmbientRingHom A (CommAlgCat.of A L)).comp (normalizationGaloisRingHom A K L σ) =
      (galoisAutomorphismRingHom K L σ).comp
        (normalizationAmbientRingHom A (CommAlgCat.of A L))

Module documentation

Ambient field automorphisms on normalizations

Declarations

normalizationGaloisGroupMap

normalizationGaloisRingHom

normalizationGaloisRingHom_commutes