Module

QuasiFinite.lean

Nyll.SchemeTheory.Morphisms.QuasiFinite

1 declaration indexed from sourceView source ↗

Module documentation

Quasi-finiteness from formal unramifiedness

A formally unramified morphism locally of finite type is locally quasi-finite.

Imports4

Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Mathlib.RingTheory.Unramified.LocalStructure
Mathlib.Tactic.Algebraize

Imported by4

theorem

of_formallyUnramified_of_locallyOfFiniteType

L33 ↗

AlgebraicGeometry.LocallyQuasiFinite.of_formallyUnramified_of_locallyOfFiniteType

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace LocallyQuasiFinite_of_formallyUnramified_of_locallyOfFiniteType
open AlgebraicGeometry CategoryTheory

Lean source · statement

theorem _root_.AlgebraicGeometry.LocallyQuasiFinite.of_formallyUnramified_of_locallyOfFiniteType
    {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y)
    [AlgebraicGeometry.FormallyUnramified f] [AlgebraicGeometry.LocallyOfFiniteType f] :
    AlgebraicGeometry.LocallyQuasiFinite f

Module documentation

Quasi-finiteness from formal unramifiedness

Declarations

of_formallyUnramified_of_locallyOfFiniteType