Module

DominantBaseChange.lean

Nyll.SchemeTheory.Morphisms.DominantBaseChange

1 declaration indexed from sourceView source ↗

Module documentation

Dominance under open base change

The range of a pullback projection is the inverse image of the range of the other morphism. Since an open map pulls dense sets back to dense sets, base change along an open morphism preserves dominance.

Imports3

Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.Topology.Maps.Basic

Imported by7

lemma

isDominant_pullback_fst_of_isOpenMap

L30 ↗

AlgebraicGeometry.isDominant_pullback_fst_of_isOpenMap

Documentation

Base change along a morphism with open underlying map preserves dominance.

Source context 4 commands

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

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

Lean source · statement

lemma isDominant_pullback_fst_of_isOpenMap {X Y S : Scheme.{u}}
    (f : X ⟶ S) (g : Y ⟶ S) (hf : IsOpenMap f) [IsDominant g] :
    IsDominant (pullback.fst f g)

Module documentation

Dominance under open base change

Declarations

isDominant_pullback_fst_of_isOpenMap