Mathlib Map

Theorems · Theorem · algebraic geometry

AlgebraicGeometry.HasAffineProperty.diagonal_iff

∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y}
  [inst : AlgebraicGeometry.IsAffine Y], Q.diagonal f ↔ P.diagonal f
Defined in
Mathlib.AlgebraicGeometry.Morphisms.Constructors
Cited by
1 results in Mathlib
Foundations
Depth 179 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AlgebraicGeometry.HasAffinePropertyAlgebraicGeometry.IsAffine
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_of_openCover_source · cited by 1AffineTargetMorphismPrope…Quiver.Hom · cited by 32603Quiver.HomCategoryTheory.CategoryStruct.id · cited by 6235CategoryStruct.idAlgebraicGeometry.Scheme · cited by 2540AlgebraicGeometry.SchemeCategoryTheory.MorphismProperty · cited by 2179CategoryTheory.MorphismPr…CategoryTheory.Category.comp_id · cited by 2119Category.comp_idCategoryTheory.Limits.pullback · cited by 864Limits.pullbackCategoryTheory.PreZeroHypercover.I₀ · cited by 763PreZeroHypercover.I₀CategoryTheory.PreZeroHypercover.X · cited by 649PreZeroHypercover.XCategoryTheory.Limits.pullback.fst · cited by 639pullback.fstCategoryTheory.Limits.pullback.snd · cited by 637pullback.sndCategoryTheory.PreZeroHypercover.f · cited by 542PreZeroHypercover.fAlgebraicGeometry.IsOpenImmersion · cited by 476AlgebraicGeometry.IsOpenI…CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover · cited by 469ZeroHypercover.toPreZeroH…CategoryTheory.inv · cited by 467CategoryTheory.invAlgebraicGeometry.Scheme.precoverage · cited by 336Scheme.precoverageHasAffineProperty.diagonal_iffCITED BYCITES

Cites31

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

Cited by1

Results whose statement or proof uses this declaration.