Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.toSigma

{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    [inst : AlgebraicGeometry.IsZariskiLocalAtSource P] →
      [inst_1 : UnivLE.{v, u}] →
        (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S) → 𝒰 ⟶ 𝒰.sigma

𝒰 refines the single object cover defined by 𝒰.

Defined in: Mathlib.AlgebraicGeometry.Cover.Sigma
Cited by: 2 results in Mathlib
Foundations: Depth 183 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AlgebraicGeometry.IsZariskiLocalAtSource UnivLE

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement · cited by 32,603
AlgebraicGeometry.Schemestatement and proof · cited by 2,540
CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
CategoryTheory.PreZeroHypercover.I₀proof · cited by 763
CategoryTheory.PreZeroHypercover.Xproof · cited by 649
CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercoverproof · cited by 469
AlgebraicGeometry.Scheme.precoveragestatement and proof · cited by 336
CategoryTheory.Limits.Sigma.ιproof · cited by 205
AlgebraicGeometry.Scheme.Coverstatement and proof · cited by 88
UnivLEstatement and proof · cited by 38
AlgebraicGeometry.IsZariskiLocalAtSourcestatement and proof · cited by 37
AlgebraicGeometry.Scheme.Cover.sigmastatement · cited by 12

Cited by2

Results whose statement or proof uses this declaration.

AlgebraicGeometry.Scheme.Cover.toSigma_h₀statement and proof · cited by 0
AlgebraicGeometry.Scheme.Cover.toSigma_s₀statement and proof · cited by 0