NYLL
Module

ConnectedFiberFullyFaithful.lean

Nyll.SchemeTheory.FiniteEtale.ConnectedFiberFullyFaithful
1 declaration indexed from sourceView source ↗

Module documentation

Full faithfulness for universally open maps with connected geometric fibres

The actual descent of finite etale sections supplies fullness through the finite etale internal Hom. Surjectivity of a geometrically connected map supplies faithfulness. Neither source nor target is assumed connected.

Imports4
Imported by2

Declarations

def

pullbackFullyFaithful_of_universallyOpen_geometricallyConnected

L30 ↗
AlgebraicGeometry.FiniteEtale.pullbackFullyFaithful_of_universallyOpen_geometricallyConnected
Documentation

A universally open morphism with geometrically connected fibres induces a fully faithful pullback functor on finite etale covers of an arbitrary base.

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
def pullbackFullyFaithful_of_universallyOpen_geometricallyConnected
    {X S : Scheme.{u}} (f : X ⟶ S) [UniversallyOpen f] [GeometricallyConnected f] :
    (FiniteEtale.pullback f).FullyFaithful

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