Module

FiniteDescent.lean

Nyll.SchemeTheory.Morphisms.FiniteDescent

1 declaration indexed from sourceView source ↗

Module documentation

Finiteness after surjective descent of an integral composite

If a separated étale morphism becomes integral after precomposition with a surjective morphism, it is universally closed. It is consequently proper and locally quasi-finite, hence finite by Zariski's main theorem.

Imports10

Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.Integral
Mathlib.AlgebraicGeometry.Morphisms.Proper
Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Mathlib.RingTheory.RingHom.Etale
Mathlib.RingTheory.RingHom.QuasiFinite
Mathlib.RingTheory.Unramified.LocalStructure

Imported by1

Nyll.SchemeTheory.Morphisms.All

theorem

of_surjective_of_comp_isIntegralHom

L38 ↗

AlgebraicGeometry.IsFinite.of_surjective_of_comp_isIntegralHom

Documentation

A separated étale morphism is finite if it is dominated surjectively by a scheme whose composite map to the base is integral.

Source context 4 commands

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

@[expose] public section
open CategoryTheory
universe u
namespace AlgebraicGeometry.IsFinite

Lean source · statement

theorem of_surjective_of_comp_isIntegralHom
    {U V Y : Scheme.{u}} (h : U ⟶ V) (g : V ⟶ Y)
    [Surjective h] [IsIntegralHom (h ≫ g)] [Etale g] [IsSeparated g] :
    IsFinite g

Module documentation

Finiteness after surjective descent of an integral composite

Declarations

of_surjective_of_comp_isIntegralHom