Module

Scheme_existsUnique_hom_sigma_of_disjoint_iSup_eq_top.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_existsUnique_hom_sigma_of_disjoint_iSup_eq_top

1 declaration indexed from sourceView source ↗

Module documentation

Scheme exists Unique hom sigma of disjoint i Sup eq top

Imports4

Mathlib.AlgebraicGeometry.Gluing
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Imported by3

theorem

existsUnique_hom_sigma_of_disjoint_iSup_eq_top

L31 ↗

AlgebraicGeometry.Scheme.existsUnique_hom_sigma_of_disjoint_iSup_eq_top

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_existsUnique_hom_sigma_of_disjoint_iSup_eq_top
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.existsUnique_hom_sigma_of_disjoint_iSup_eq_top
    {σ : Type u} (H : σ → Scheme.{u}) {T : Scheme.{u}} (U : σ → T.Opens)
    (hdisj : ∀ i j, i ≠ j → Disjoint (U i) (U j)) (hcov : (⨆ i, U i) = ⊤)
    (v : ∀ i, ((U i : T.Opens) : Scheme.{u}) ⟶ H i) :
    ∃! u : T ⟶ ∐ H, ∀ i, (U i).ι ≫ u = v i ≫ Sigma.ι H i

Module documentation

Scheme exists Unique hom sigma of disjoint i Sup eq top

Declarations

existsUnique_hom_sigma_of_disjoint_iSup_eq_top