Module

TensorBaseChange.lean

Nyll.SchemeTheory.FiniteEtale.Away.TensorBaseChange

2 declarations indexed from sourceView source ↗

Module documentation

Base change of a literal etale away map

The complement hypothesis on a finite normalization is stated using the literal map between two away localizations. This file transports that map through a pushout. The proof pastes the original pushout with the four canonical localization squares, so it never assumes that the unlocalized map is etale.

Imports2

Mathlib.RingTheory.RingHom.Etale
Mathlib.RingTheory.Localization.BaseChange

Imported by5

theorem

localization_awayMap_etale_of_isPushout

L31 ↗

EtaleFundamentalGroups.localization_awayMap_etale_of_isPushout

Documentation

A literal etale away map remains etale in any pushout square. All localization algebras are constructed internally, and the conclusion is the literal Localization.awayMap for the lower horizontal map.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uA uB uC uD

Lean source · statement

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

theorem

localization_awayMap_tensorProduct_etale

L186 ↗

EtaleFundamentalGroups.localization_awayMap_tensorProduct_etale