Documentation Verification Report

UniversallyInjective

📁 Source: Mathlib/AlgebraicGeometry/Morphisms/UniversallyInjective.lean

Statistics

Metric	Count
Definitions `UniversallyInjective`	1
Theorems `injective`, `iff_diagonal`, `isStableUnderBaseChange`, `respectsIso`, `universally_injective`, `instIsMultiplicativeSchemeUniversallyInjective`, `instUniversallyInjectiveOfMonoScheme`, `universallyInjective_eq`, `universallyInjective_eq_diagonal`, `universallyInjective_iff`, `universallyInjective_isStableUnderComposition`, `universallyInjective_isZariskiLocalAtTarget`	12
Total	13

AlgebraicGeometry

Definitions

Name	Category	Theorems
`UniversallyInjective` 📖	CompData	11 math math: `UniversallyInjective.iff_diagonal`, `instUniversallyInjectiveOfMonoScheme`, `universallyInjective_isZariskiLocalAtTarget`, `universallyInjective_iff`, `universallyInjective_eq`, `instIsMultiplicativeSchemeUniversallyInjective`, `UniversallyInjective.respectsIso`, `universallyInjective_eq_diagonal`, `universallyInjective_isStableUnderComposition`, `UniversallyInjective.isStableUnderBaseChange`, `descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsMultiplicativeSchemeUniversallyInjective` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `Scheme` `Scheme.instCategory` `UniversallyInjective`	—	`instUniversallyInjectiveOfMonoScheme` `IsOpenImmersion.mono` `IsOpenImmersion.of_isIso` `CategoryTheory.IsIso.id` `universallyInjective_isStableUnderComposition`
`instUniversallyInjectiveOfMonoScheme` 📖	mathematical	—	`UniversallyInjective`	—	`Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.isIso_diagonal_iff` `UniversallyInjective.iff_diagonal` `instSurjectiveOfIsIsoScheme`
`universallyInjective_eq` 📖	mathematical	—	`UniversallyInjective` `CategoryTheory.MorphismProperty.universally` `Scheme` `Scheme.instCategory` `topologically`	—	`universallyInjective_iff`
`universallyInjective_eq_diagonal` 📖	mathematical	—	`UniversallyInjective` `CategoryTheory.MorphismProperty.diagonal` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullbacks` `Surjective`	—	`le_antisymm` `Scheme.Pullback.instHasPullbacks` `Scheme.Pullback.instHasPullback` `UniversallyInjective.universally_injective` `CategoryTheory.IsPullback.of_hasPullback` `Scheme.Hom.comp_apply` `CategoryTheory.Limits.pullback.diagonal_fst` `CategoryTheory.MorphismProperty.universally_eq_iff` `CategoryTheory.MorphismProperty.IsStableUnderBaseChange.diagonal` `Surjective.instIsStableUnderBaseChangeScheme` `instRespectsIsoSchemeSurjective` `universallyInjective_eq` `CategoryTheory.MorphismProperty.universally_mono` `Scheme.Pullback.exists_preimage_pullback` `Surjective.surj` `CategoryTheory.Limits.pullback.diagonal_snd`
`universallyInjective_iff` 📖	mathematical	—	`UniversallyInjective` `CategoryTheory.MorphismProperty.universally` `Scheme` `Scheme.instCategory` `topologically`	—	—
`universallyInjective_isStableUnderComposition` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `Scheme` `Scheme.instCategory` `UniversallyInjective`	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition.universally` `Scheme.Pullback.instHasPullbacks` `injective_isStableUnderComposition` `universallyInjective_eq`
`universallyInjective_isZariskiLocalAtTarget` 📖	mathematical	—	`IsZariskiLocalAtTarget` `UniversallyInjective`	—	`Scheme.Pullback.instHasPullbacks` `instIsZariskiLocalAtTargetDiagonalScheme` `surjective_isZariskiLocalAtTarget` `universallyInjective_eq_diagonal`

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injective` 📖	mathematical	—	`TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'`	—	`AlgebraicGeometry.UniversallyInjective.universally_injective` `CategoryTheory.IsPullback.of_id_snd`

AlgebraicGeometry.UniversallyInjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_diagonal` 📖	mathematical	—	`AlgebraicGeometry.UniversallyInjective` `AlgebraicGeometry.Surjective` `CategoryTheory.Limits.pullback.diagonalObj` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.diagonal`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.Scheme.Pullback.instHasPullbacks` `AlgebraicGeometry.universallyInjective_eq_diagonal`
`isStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.UniversallyInjective`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullbacks` `CategoryTheory.MorphismProperty.IsStableUnderBaseChange.diagonal` `AlgebraicGeometry.Surjective.instIsStableUnderBaseChangeScheme` `AlgebraicGeometry.instRespectsIsoSchemeSurjective` `AlgebraicGeometry.universallyInjective_eq_diagonal`
`respectsIso` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.UniversallyInjective`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullbacks` `CategoryTheory.MorphismProperty.RespectsIso.diagonal` `AlgebraicGeometry.instRespectsIsoSchemeSurjective` `AlgebraicGeometry.universallyInjective_eq_diagonal`
`universally_injective` 📖	mathematical	—	`CategoryTheory.MorphismProperty.universally` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.topologically`	—	—

---

← Back to Index