NYLL
Module

NativeNormalizationOriginalAction.lean

Nyll.EtaleFundamentalGroups.Inertia.NativeNormalizationOriginalAction
2 declarations indexed from sourceView source ↗

Module documentation

Original normalization actions on native coefficient fields

The native coefficient algebra owns the ring and coefficient action. Its field structure is opened only here. Restriction of the original field action is compared with normalization functoriality through their literal injective coefficient inclusion.

Imports3
Imported by2

Declarations

def

nativeNormalizationOriginalAction

L37 ↗
EtaleFundamentalGroups.Inertia.nativeNormalizationOriginalAction
Documentation

The prescribed integral-closure action, on the native normalization carrier, with no finite-intermediate-field structure opened by its caller.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) [CommRing A] [Field K]
  [Algebra A K] [IsFractionRing A K]
  (C : CommAlgCat.{w} A) (hC : IsField C.carrier)
  [Algebra K C.carrier] [tAKC : IsScalarTower A K C.carrier]
  [Algebra.IsAlgebraic K C.carrier]
Lean source · statement
def nativeNormalizationOriginalAction :
    MulSemiringAction (galoisGroupObject K C.carrier).carrier
      (normalizationCommAlgCat A C.carrier).carrier
theorem

nativeNormalizationOriginalAction_ringHom

L45 ↗
EtaleFundamentalGroups.Inertia.nativeNormalizationOriginalAction_ringHom
Documentation

The prescribed action agrees with the existing normalization group map. The equality is proved on actual coefficients, rather than supplied.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) [CommRing A] [Field K]
  [Algebra A K] [IsFractionRing A K]
  (C : CommAlgCat.{w} A) (hC : IsField C.carrier)
  [Algebra K C.carrier] [tAKC : IsScalarTower A K C.carrier]
  [Algebra.IsAlgebraic K C.carrier]
Lean source · full declaration
theorem nativeNormalizationOriginalAction_ringHom
    (g : (galoisGroupObject K C.carrier).carrier) :
    let : MulSemiringAction (galoisGroupObject K C.carrier).carrier
        (normalizationCommAlgCat A C.carrier).carrier :=
      nativeNormalizationOriginalAction A K C hC
    MulSemiringAction.toRingHom (galoisGroupObject K C.carrier).carrier
        (normalizationCommAlgCat A C.carrier).carrier g =
      commAlgAutomorphismRingHom A (normalizationCommAlgCat A C.carrier)
        ((normalizationAutomorphismGroupMap A C).hom'.toFun
          ((scalarRestrictionGroupMap A K C).hom'.toFun g)) := by
  intro nativeAction
  let : Field C.carrier := hC.toField
  apply (RingHom.cancel_left (g := normalizationAmbientRingHom A C)
    Subtype.val_injective).mp
  exact (normalizationCommAlg_action_comp_inclusion A K C.carrier g).symm.trans
    (normalizationGaloisRingHom_commutes A K C.carrier g).symm

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