Theorems · Theorem · algebraic geometry

AlgebraicGeometry.isOpenImmersion_sigmaDesc

∀ {σ : Type v} (g : σ → AlgebraicGeometry.Scheme) [inst : Small.{u, v} σ] {X : AlgebraicGeometry.Scheme}
  (α : (i : σ) → g i ⟶ X) [∀ (i : σ), AlgebraicGeometry.IsOpenImmersion (α i)],
  Pairwise (Function.onFun Disjoint fun x => Set.range ⇑(α x)) →
    AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.Sigma.desc α)

Defined in

Mathlib.AlgebraicGeometry.Limits

Cited by

1 results in Mathlib

Foundations

Depth 180 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SmallAlgebraicGeometry.IsOpenImmersion