Module

ClosedDiscreteRestrictionMono.lean

Nyll.SchemeTheory.Topology.ClosedDiscreteRestrictionMono

1 declaration indexed from sourceView source ↗

Module documentation

The supported-function pullback comparison is a monomorphism

On the closed support the actual comparison identifies stalk evaluations. Outside the support its source stalk is terminal, so its stalk map is automatically a monomorphism. Stalks then detect that the actual sheaf comparison is a monomorphism. This is enough to transfer the concrete function-extension result to the actual inverse-image unit. The Lean proof is original.

Imports7

Mathlib.CategoryTheory.Iso
Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Mathlib.Topology.Sheaves.Stalks
Nyll.SchemeTheory.Topology.ClosedDiscreteSheaf
Nyll.SchemeTheory.Topology.ClosedDiscreteRestriction
Nyll.SchemeTheory.Topology.ClosedDiscreteStalkOutside
Nyll.SchemeTheory.Topology.SheafPullbackStalks

Imported by2

theorem

mono_closedDiscretePullbackMap

L36 ↗

SchemeTheory.mono_closedDiscretePullbackMap

Documentation

The actual adjoint of restriction on a closed discrete-function support is a monomorphism; no geometric base-change hypothesis is assumed.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopologicalSpace
namespace SchemeTheory

Lean source · statement

theorem mono_closedDiscretePullbackMap {X Y : TopCat.{u}}
    (f : X ⟶ Y) (C : Set Y) (hC : IsClosed C) (A : Type u) :
    Mono (closedDiscretePullbackMap f C A)

Module documentation

The supported-function pullback comparison is a monomorphism

Declarations

mono_closedDiscretePullbackMap