Module

EtaleExtension.lean

Nyll.SchemeTheory.FiniteEtale.Away.EtaleExtension

1 declaration indexed from sourceView source ↗

Module documentation

Boundary Away maps through an etale extension

The boundary Away property is stable under a genuinely etale extension of the target. This elementary map-level statement is useful after a Tag/ETag comparison has produced the primitive Away map on one local factor and a retained unit factor supplies an etale algebra over that same factor.

Unlike the formally-etale localization bridge, no module-finiteness or Noetherian hypothesis is needed: after localizing both targets at the same source element, the second map is etale by localization and restriction of scalars, and the two literal Away maps compose.

Imports3

Mathlib.RingTheory.Etale.Basic
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.RingHom.Etale

Imported by3

theorem

localization_awayMap_etale_of_etale_extension

L38 ↗

EtaleFundamentalGroups.localization_awayMap_etale_of_etale_extension

Documentation

A literal boundary Away map remains etale after a genuinely etale target extension.

This is deliberately stated for the actual composite algebra map. It does not replace either target by an abstractly equivalent algebra, and it does not require the intermediate or final algebra to be finite over the original base.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uC uD

Lean source · statement

theorem localization_awayMap_etale_of_etale_extension
    {A : Type uA} {C : Type uC} {D : Type uD}
    [CommRing A] [CommRing C] [CommRing D]
    [Algebra A C] [Algebra C D] [Algebra A D]
    [IsScalarTower A C D]
    [Algebra.Etale C D]
    (f : A)
    (hAway : (Localization.awayMap (algebraMap A C) f).Etale) :
    (Localization.awayMap (algebraMap A D) f).Etale

Module documentation

Boundary Away maps through an etale extension

Declarations

localization_awayMap_etale_of_etale_extension