Module

FiniteLimits.lean

Nyll.SchemeTheory.FiniteEtale.Forget.FiniteLimits

3 declarations indexed from sourceView source ↗

Module documentation

This file records the limit-preservation part of Stacks Project, Tag 0BNA, directly for the canonical forgetful functor from finite étale schemes.

Imports3

Imported by5

instance

AlgebraicGeometry.FiniteEtale.forgetPreservesFiniteLimits

Documentation

The canonical forgetful functor from finite étale schemes over X to schemes over X preserves finite limits.

Source context 5 commands

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

@[expose] public section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})

Lean source · statement

instance forgetPreservesFiniteLimits :
    PreservesFiniteLimits (forget X)

instance

AlgebraicGeometry.FiniteEtale.forgetCompOverForgetPreservesPullbacks

Documentation

Forgetting a finite étale scheme all the way to schemes preserves pullbacks.

Source context 5 commands

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

@[expose] public section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})

Lean source · statement

instance forgetCompOverForgetPreservesPullbacks :
    PreservesLimitsOfShape WalkingCospan
      (forget X ⋙ CategoryTheory.Over.forget X)

instance

AlgebraicGeometry.FiniteEtale.forgetCompOverForgetPreservesEqualizers

Documentation

Forgetting a finite étale scheme all the way to schemes preserves equalizers.

Source context 5 commands

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

@[expose] public section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})

Lean source · statement

instance forgetCompOverForgetPreservesEqualizers :
    PreservesLimitsOfShape WalkingParallelPair
      (forget X ⋙ CategoryTheory.Over.forget X)