Module

BoundaryAwayFieldEquiv.lean

Nyll.EtaleFundamentalGroups.Normalization.IntegralClosure.BoundaryAwayFieldEquiv

1 declaration indexed from sourceView source ↗

Module documentation

Transporting normalization boundary-away maps across field equivalences

When a map in a scalar tower of fields is bijective, it gives an algebra equivalence of the ambient fields. Mapping integral closures along that equivalence transports the literal boundary-away etaleness statement.

Imports1

Nyll.SchemeTheory.FiniteEtale.Away.AlgEquivTransport

Imported by6

theorem

integralClosure_boundaryAway_of_bijective_fieldTower_algebraMap

L25 ↗

EtaleFundamentalGroups.integralClosure_boundaryAway_of_bijective_fieldTower_algebraMap

Documentation

A source-produced bijective field map transports the primitive boundary-away map between the corresponding integral closures.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uL uP

Lean source · statement

theorem integralClosure_boundaryAway_of_bijective_fieldTower_algebraMap
    {A : Type uA} {L : Type uL} {P : Type uP}
    [CommRing A] [Field L] [Field P]
    [Algebra A L] [Algebra A P]
    [Algebra L P] [IsScalarTower A L P]
    (hbij : Function.Bijective (algebraMap L P))
    (f : A)
    (hAway :
      (Localization.awayMap
        (algebraMap A (integralClosure A L)) f).Etale) :
    (Localization.awayMap
      (algebraMap A (integralClosure A P)) f).Etale

Module documentation

Transporting normalization boundary-away maps across field equivalences

Declarations

integralClosure_boundaryAway_of_bijective_fieldTower_algebraMap