Documentation Verification Report

SchemeTheoreticallyDominant

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

Statistics

Metric	Count
Definitions `IsSchemeTheoreticallyDominant`	1
Theorems `isReduced`, `ker_eq_bot`, `of_isDominant`, `of_isPullback`, `pullbackFst`, `pullbackSnd`, `app_injective`, `ker_eq_bot`, `instIsDominantOfIsSchemeTheoreticallyDominantOfQuasiCompact`, `instIsMultiplicativeSchemeIsSchemeTheoreticallyDominant`, `instIsSchemeTheoreticallyDominantCompScheme`, `instIsSchemeTheoreticallyDominantOfIsIsoScheme`, `isSchemeTheoreticallyDominant_iff`, `isSchemeTheoreticallyDominant_iff_isDominant`	14
Total	15

AlgebraicGeometry

Definitions

Name	Category	Theorems
`IsSchemeTheoreticallyDominant` 📖	CompData	9 math math: `instIsMultiplicativeSchemeIsSchemeTheoreticallyDominant`, `IsSchemeTheoreticallyDominant.pullbackSnd`, `isSchemeTheoreticallyDominant_iff`, `IsSchemeTheoreticallyDominant.of_isDominant`, `IsSchemeTheoreticallyDominant.of_isPullback`, `isSchemeTheoreticallyDominant_iff_isDominant`, `IsSchemeTheoreticallyDominant.pullbackFst`, `instIsSchemeTheoreticallyDominantOfIsIsoScheme`, `instIsSchemeTheoreticallyDominantCompScheme`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsDominantOfIsSchemeTheoreticallyDominantOfQuasiCompact` 📖	mathematical	—	`IsDominant`	—	`isDominant_iff` `DenseRange.eq_1` `dense_iff_closure_eq` `Scheme.Hom.support_ker` `Scheme.Hom.ker_eq_bot` `Scheme.IdealSheafData.support_bot` `TopologicalSpace.Closeds.coe_top`
`instIsMultiplicativeSchemeIsSchemeTheoreticallyDominant` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `Scheme` `Scheme.instCategory` `IsSchemeTheoreticallyDominant`	—	`instIsSchemeTheoreticallyDominantOfIsIsoScheme` `CategoryTheory.IsIso.id` `instIsSchemeTheoreticallyDominantCompScheme`
`instIsSchemeTheoreticallyDominantCompScheme` 📖	mathematical	—	`IsSchemeTheoreticallyDominant` `CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory`	—	`isSchemeTheoreticallyDominant_iff` `Scheme.Hom.ker_comp` `Scheme.Hom.ker_eq_bot` `Scheme.IdealSheafData.map_bot`
`instIsSchemeTheoreticallyDominantOfIsIsoScheme` 📖	mathematical	—	`IsSchemeTheoreticallyDominant`	—	`Scheme.Hom.ker_eq_bot_of_isIso`
`isSchemeTheoreticallyDominant_iff` 📖	mathematical	—	`IsSchemeTheoreticallyDominant` `Scheme.Hom.ker` `Bot.bot` `Scheme.IdealSheafData` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `Scheme.IdealSheafData.instPartialOrder` `Scheme.IdealSheafData.instOrderBot`	—	—
`isSchemeTheoreticallyDominant_iff_isDominant` 📖	mathematical	—	`IsSchemeTheoreticallyDominant` `IsDominant`	—	`instIsDominantOfIsSchemeTheoreticallyDominantOfQuasiCompact` `IsSchemeTheoreticallyDominant.of_isDominant`

AlgebraicGeometry.IsSchemeTheoreticallyDominant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isReduced` 📖	mathematical	—	`AlgebraicGeometry.IsReduced`	—	`isReduced_of_injective` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `AlgebraicGeometry.Scheme.Hom.app_injective` `AlgebraicGeometry.IsReduced.component_reduced`
`ker_eq_bot` 📖	mathematical	—	`AlgebraicGeometry.Scheme.Hom.ker` `Bot.bot` `AlgebraicGeometry.Scheme.IdealSheafData` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `AlgebraicGeometry.Scheme.IdealSheafData.instPartialOrder` `AlgebraicGeometry.Scheme.IdealSheafData.instOrderBot`	—	—
`of_isDominant` 📖	mathematical	—	`AlgebraicGeometry.IsSchemeTheoreticallyDominant`	—	`AlgebraicGeometry.isSchemeTheoreticallyDominant_iff` `AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff` `SetLike.coe_injective` `TopologicalSpace.Closeds.coe_top` `Set.univ_subset_iff` `Dense.closure_eq` `AlgebraicGeometry.Scheme.Hom.denseRange` `IsClosed.closure_subset_iff` `TopologicalSpace.Closeds.isClosed` `AlgebraicGeometry.Scheme.Hom.range_subset_ker_support`
`of_isPullback` 📖	mathematical	`CategoryTheory.IsPullback` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	`AlgebraicGeometry.IsSchemeTheoreticallyDominant`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.IsPullback.isoPullback_hom_snd` `AlgebraicGeometry.instIsSchemeTheoreticallyDominantCompScheme` `AlgebraicGeometry.instIsSchemeTheoreticallyDominantOfIsIsoScheme` `CategoryTheory.Iso.isIso_hom` `pullbackSnd`
`pullbackFst` 📖	mathematical	—	`AlgebraicGeometry.IsSchemeTheoreticallyDominant` `CategoryTheory.Limits.pullback` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.fst`	—	`of_isPullback` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.IsPullback.flip` `CategoryTheory.IsPullback.of_hasPullback`
`pullbackSnd` 📖	mathematical	—	`AlgebraicGeometry.IsSchemeTheoreticallyDominant` `CategoryTheory.Limits.pullback` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.snd`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.isSchemeTheoreticallyDominant_iff` `TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le` `AlgebraicGeometry.Scheme.isBasis_affineOpens` `TopologicalSpace.IsOpenCover.comap` `TopologicalSpace.Opens.IsBasis.isOpenCover` `AlgebraicGeometry.Scheme.IdealSheafData.ext_of_iSup_eq_top` `RingHom.instRingHomClass` `AlgebraicGeometry.Scheme.Hom.ker_apply` `AlgebraicGeometry.instQuasiCompactSndScheme` `le_rfl` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `CommRingCat.Colimits.hasColimits_commRingCat` `CategoryTheory.IsPullback.of_hasPullback` `AlgebraicGeometry.Scheme.Hom.comp_preimage` `CategoryTheory.Limits.pullback.condition` `right_eq_inf` `le_imp_le_of_le_of_le` `AlgebraicGeometry.Scheme.Hom.preimage_mono` `le_refl` `AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right` `AlgebraicGeometry.Scheme.Hom.isCompact_preimage` `AlgebraicGeometry.IsAffineOpen.isCompact` `CommRingCat.inr_injective_of_flat` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `AlgebraicGeometry.Scheme.Hom.app_injective` `AlgebraicGeometry.Scheme.Hom.flat_appLE` `CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `CommRingCat.forget_preservesLimits` `CategoryTheory.Limits.colimit.ι_desc` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass`

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`app_injective` 📖	mathematical	—	`CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `AlgebraicGeometry.Scheme.Opens` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `app`	—	`RingHom.instRingHomClass` `RingHom.injective_iff_ker_eq_bot` `ker_apply` `ker_eq_bot` `injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `TopCat.Presheaf.IsSheaf.section_ext` `CommRingCat.hasLimits` `CommRingCat.forget_preservesLimits` `CommRingCat.forgetReflectIsos` `AlgebraicGeometry.SheafedSpace.IsSheaf` `TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open` `AlgebraicGeometry.Scheme.isBasis_affineOpens` `TopologicalSpace.Opens.isOpen` `CategoryTheory.ConcreteCategory.comp_apply` `naturality` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`ker_eq_bot` 📖	mathematical	—	`ker` `Bot.bot` `AlgebraicGeometry.Scheme.IdealSheafData` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `AlgebraicGeometry.Scheme.IdealSheafData.instPartialOrder` `AlgebraicGeometry.Scheme.IdealSheafData.instOrderBot`	—	`AlgebraicGeometry.IsSchemeTheoreticallyDominant.ker_eq_bot`

---

← Back to Index