Module

BoundaryAway.lean

Nyll.EtaleFundamentalGroups.Normalization.IntegralClosure.IntegralBase.BoundaryAway

4 declarations indexed from sourceView source ↗

Module documentation

Boundary-away transport through a finite integral base

For a finite base enlargement inside one field, the two integral closures are canonically equivalent. Localizing that equivalence at a primitive element transports etaleness of the literal away map to the normalization over the enlarged base.

Imports2

Imported by3

theorem

integralClosure_integralBase_boundaryAway

L27 ↗

EtaleFundamentalGroups.integralClosure_integralBase_boundaryAway

Documentation

The primitive away property of a normalization is unchanged after a finite integral enlargement of the base inside the same ambient field.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uB uL

Lean source · statement

theorem integralClosure_integralBase_boundaryAway
    {A : Type uA} {B : Type uB} {L : Type uL}
    [CommRing A] [CommRing B] [Field L]
    [Algebra A B] [Module.Finite A B]
    [Algebra A L] [Algebra B L] [IsScalarTower A B L]
    (f : A)
    (hAway :
      (Localization.awayMap
        (algebraMap A (integralClosure A L)) f).Etale) :
    (Localization.awayMap
      (algebraMap A (integralClosure B L)) f).Etale

theorem

integralClosure_integralBase_boundaryAway_comp

L85 ↗

EtaleFundamentalGroups.integralClosure_integralBase_boundaryAway_comp

Documentation

Map-explicit form of integral-base boundary-away transport: the target map is the literal composite through the enlarged base.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uB uL

Lean source · statement

theorem integralClosure_integralBase_boundaryAway_comp
    {A : Type uA} {B : Type uB} {L : Type uL}
    [CommRing A] [CommRing B] [Field L]
    [Algebra A B] [Module.Finite A B]
    [Algebra A L] [Algebra B L] [IsScalarTower A B L]
    (f : A)
    (hAway :
      (Localization.awayMap
        (algebraMap A (integralClosure A L)) f).Etale) :
    (Localization.awayMap
      ((algebraMap B (integralClosure B L)).comp (algebraMap A B))
      f).Etale

theorem

integralClosure_integralBase_boundaryAway_of_bijective_fieldTower_algebraMap

L109 ↗

EtaleFundamentalGroups.integralClosure_integralBase_boundaryAway_of_bijective_fieldTower_algebraMap

Documentation

A sourced comparison of ambient fields followed by a finite integral base enlargement preserves the primitive boundary-away map.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uB uL

Lean source · statement

theorem
    integralClosure_integralBase_boundaryAway_of_bijective_fieldTower_algebraMap
    {A : Type uA} {B : Type uB}
    {Omega : Type uL} {P : Type*}
    [CommRing A] [CommRing B] [Field Omega] [Field P]
    [Algebra A Omega]
    [Algebra Omega P] [Algebra A P] [IsScalarTower A Omega P]
    [Algebra A B] [Module.Finite A B]
    [Algebra B P] [IsScalarTower A B P]
    (hbij : Function.Bijective (algebraMap Omega P))
    (f : A)
    (hAway :
      (Localization.awayMap
        (algebraMap A (integralClosure A Omega)) f).Etale) :
    (Localization.awayMap
      (algebraMap A (integralClosure B P)) f).Etale

theorem

integralClosure_integralBase_boundaryAway_comp_of_bijective_fieldTower_algebraMap

L135 ↗

EtaleFundamentalGroups.integralClosure_integralBase_boundaryAway_comp_of_bijective_fieldTower_algebraMap

Documentation

Map-explicit form of the preceding transport: the target map is written as the literal composite through the finite integral base.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uB uL

Lean source · statement

theorem
    integralClosure_integralBase_boundaryAway_comp_of_bijective_fieldTower_algebraMap
    {A : Type uA} {B : Type uB}
    {Omega : Type uL} {P : Type*}
    [CommRing A] [CommRing B] [Field Omega] [Field P]
    [Algebra A Omega]
    [Algebra Omega P] [Algebra A P] [IsScalarTower A Omega P]
    [Algebra A B] [Module.Finite A B]
    [Algebra B P] [IsScalarTower A B P]
    (hbij : Function.Bijective (algebraMap Omega P))
    (f : A)
    (hAway :
      (Localization.awayMap
        (algebraMap A (integralClosure A Omega)) f).Etale) :
    (Localization.awayMap
      ((algebraMap B (integralClosure B P)).comp (algebraMap A B))
      f).Etale

Module documentation

Boundary-away transport through a finite integral base

Declarations

integralClosure_integralBase_boundaryAway

integralClosure_integralBase_boundaryAway_comp

integralClosure_integralBase_boundaryAway_of_bijective_fieldTower_algebraMap

integralClosure_integralBase_boundaryAway_comp_of_bijective_fieldTower_algebraMap