NYLL
Module

ScalarRestrictionGroupMap.lean

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

Module documentation

Restriction of scalars on automorphism groups

Bundles algebra automorphisms as group objects and constructs the group morphism that restricts their scalars along an algebra tower.

Imports4
Imported by8

Declarations

def

galoisGroupObject

L26 ↗
SchemeTheory.galoisGroupObject
Documentation

The actual Galois automorphism group, retained as its native group object.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
Lean source · statement
def galoisGroupObject (K : Type u) (L : Type v)
    [CommRing K] [CommRing L] [Algebra K L] : GrpCat.{v}
def

scalarRestrictionGroupMap

L31 ↗
SchemeTheory.scalarRestrictionGroupMap
Documentation

Restricting the original K-linear action to its original A-coefficients.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
Lean source · full declaration
def scalarRestrictionGroupMap
    (A : Type u) (K : Type v) [CommRing A] [Field K] [Algebra A K]
    (C : CommAlgCat.{w} A) [Algebra K C] [IsScalarTower A K C] :
    GrpCat.Hom (galoisGroupObject K C) (commAlgAutomorphismGroup A C) where
  hom' := AlgEquiv.restrictScalarsHom A

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