Nyll.EtaleFundamentalGroups.FiniteEtale.Away.FinitePresentationExtension

Module documentation

Boundary Away through a finitely presented formally-etale extension

The existing finite-extension transport derives finite presentation from module finiteness over a Noetherian base. Maximal-adic completions used by the one-point inertia construction do not currently carry a global IsNoetherianRing instance. This file records the exact replacement needed there: finite presentation of the final chosen factor is supplied directly.

The proof keeps the literal composite away map. Its formal etaleness is obtained by localizing the formally-etale upper map; its finite presentation is the base change of the supplied finite presentation along the away localization. No Noetherian hypothesis is used.

theorem

localization_awayMap_etale_of_finitePresentation_formallyEtale_extension

L40 ↗

EtaleFundamentalGroups.localization_awayMap_etale_of_finitePresentation_formallyEtale_extension

Documentation

A finitely presented formally-etale extension of an algebra already etale away from f remains etale for the literal composite away map.

This is the Noetherian-free form of localization_awayMap_etale_of_finite_formallyEtale_extension. In the completion application, finite presentation of the chosen factor is constructed from finite projectivity over the completed root cover and the finite-free root cover over the completed prefix.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uA uC uD

Lean source · statement

theorem
    localization_awayMap_etale_of_finitePresentation_formallyEtale_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]
    [Module.FinitePresentation A D]
    [Algebra.FormallyEtale C D]
    (f : A)
    (hAway : (Localization.awayMap (algebraMap A C) f).Etale) :
    (Localization.awayMap (algebraMap A D) f).Etale

Module documentation

Boundary Away through a finitely presented formally-etale extension

Declarations

localization_awayMap_etale_of_finitePresentation_formallyEtale_extension