NYLL
Module

IsSeparated_of_comp_of_universallyClosed_of_surjective.lean

Nyll.AlgebraicCurves.Geometry.Schemes.IsSeparated_of_comp_of_universallyClosed_of_surjective
1 declaration indexed from sourceView source ↗

Module documentation

Separatedness descends through a universally closed cover

If the first morphism is universally closed and surjective, separatedness of the composite implies separatedness of the second morphism.

Imports4
  • Mathlib.AlgebraicGeometry.Morphisms.Separated
  • Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
  • Mathlib.AlgebraicGeometry.Morphisms.Immersion
  • Mathlib.AlgebraicGeometry.Morphisms.Proper
Imported by3

Declarations

theorem

of_comp_of_universallyClosed_of_surjective

L34 ↗
AlgebraicGeometry.IsSeparated.of_comp_of_universallyClosed_of_surjective
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_of_comp_of_universallyClosed_of_surjective
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
Lean source · statement
theorem _root_.AlgebraicGeometry.IsSeparated.of_comp_of_universallyClosed_of_surjective
    {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsSeparated (f ≫ g)] [UniversallyClosed f]
    [Surjective f] : IsSeparated g

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.