Module

SectionsDescent.lean

Nyll.SchemeTheory.FiniteEtale.SectionsDescent

2 declarations indexed from sourceView source ↗

Module documentation

Descending finite étale global sections

The algebra of global sections descends as an actual finite étale algebra when it is finite étale after faithfully flat affine base change. The comparison is the pushout of the four actual maps on sections.

Imports5

Nyll.SchemeTheory.Affine.FlatBaseChangeAffinization
Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Mathlib.Algebra.Category.Ring.Constructions
Mathlib.RingTheory.Etale.Descent
Mathlib.RingTheory.Finiteness.Descent

Imported by2

theorem

of_isPushout

L33 ↗

RingHom.FiniteEtale.of_isPushout

Documentation

Descent across a specified pushout of ring maps. The three scalar structures are owned by the given maps; no second route to the same algebra structure is introduced.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace RingHom.FiniteEtale

Lean source · statement

theorem of_isPushout
    {A B C D : CommRingCat.{u}} (f : A ⟶ B) (g : A ⟶ C)
    (i : B ⟶ D) (j : C ⟶ D) (h : IsPushout f g i j)
    (hg : g.hom.FaithfullyFlat) (hj : j.hom.FiniteEtale) : f.hom.FiniteEtale

theorem

finiteEtale_appTop_of_flat_baseChange

L63 ↗

AlgebraicGeometry.finiteEtale_appTop_of_flat_baseChange