Module

DensePullback.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.DensePullback

1 declaration indexed from sourceView source ↗

Module documentation

Stacks Project, Tag 0BQE: finite étale morphisms can be distinguished after base change along any scheme morphism with dense image.

Imports1

Imported by1

theorem

AlgebraicGeometry.FiniteEtale.pullback_faithful_of_denseRange

Documentation

A scheme morphism with dense image induces a faithful functor on finite étale covers.

Source context 4 commands

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

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

Lean source · statement

theorem pullback_faithful_of_denseRange {X Y : Scheme.{u}} (f : X ⟶ Y)
    (hf : DenseRange f) : (FiniteEtale.pullback f).Faithful