NYLL
Module

AlgEquivTransport.lean

Nyll.SchemeTheory.FiniteEtale.Away.AlgEquivTransport
2 declarations indexed from sourceView source ↗

Module documentation

Transport of a literal Away map along an algebra equivalence

The chosen Tag factor and the root-refined normalization factor are related by an algebra equivalence. This file records the formal transport needed to keep the literal Away map while changing between those two carriers.

No etaleness of either unlocalized carrier is used. The proof regards an algebra equivalence as the right edge of a pushout and applies the literal Away base-change theorem.

Imports1
Imported by8

Declarations

theorem

localization_awayMap_etale_of_algEquiv

L29 ↗
EtaleFundamentalGroups.localization_awayMap_etale_of_algEquiv
Documentation

A literal etale Away map is invariant under an equivalence of its target as an algebra over the base.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uC uD₀ uD₁
Lean source · statement
theorem localization_awayMap_etale_of_algEquiv
    {A : Type uA} {D₀ : Type uD₀} {D₁ : Type uD₁}
    [CommRing A] [CommRing D₀] [CommRing D₁]
    [Algebra A D₀] [Algebra A D₁]
    (E : D₀ ≃ₐ[A] D₁) (f : A)
    (hAway :
      (Localization.awayMap (algebraMap A D₀) f).Etale) :
    (Localization.awayMap (algebraMap A D₁) f).Etale
theorem

localization_awayMap_etale_of_tower_algEquiv

L52 ↗
EtaleFundamentalGroups.localization_awayMap_etale_of_tower_algEquiv
Documentation

A target equivalence over an intermediate algebra transports the literal Away map over the original base, provided both target actions are the actual scalar-tower composites.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uC uD₀ uD₁
Lean source · statement
theorem localization_awayMap_etale_of_tower_algEquiv
    {A : Type uA} {C : Type uC}
    {D₀ : Type uD₀} {D₁ : Type uD₁}
    [CommRing A] [CommRing C] [CommRing D₀] [CommRing D₁]
    [Algebra A C]
    [Algebra C D₀] [Algebra C D₁]
    [Algebra A D₀] [Algebra A D₁]
    [IsScalarTower A C D₀] [IsScalarTower A C D₁]
    (E : D₀ ≃ₐ[C] D₁) (f : A)
    (hAway :
      (Localization.awayMap (algebraMap A D₀) f).Etale) :
    (Localization.awayMap (algebraMap A D₁) f).Etale

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.