Normalization

📁 Source: Mathlib/AlgebraicGeometry/Normalization.lean

Statistics

Metric	Count
Definitions fromNormalization, instIsIntegralHomNormalizationPullback, normalization, normalizationCoprodIso, normalizationDesc, normalizationDiagram, normalizationDiagramMap, normalizationGlueData, normalizationObjIso, normalizationOpenCover, normalizationPullback, toNormalization	12
Theorems coequifibered_normalizationDiagramMap, fromNormalization_app, fromNormalization_app_assoc, fromNormalization_preimage, inl_normalizationCoprodIso_hom_fromNormalization, inl_normalizationCoprodIso_hom_fromNormalization_assoc, inl_toNormalization_normalizationCoprodIso_inv, inl_toNormalization_normalizationCoprodIso_inv_assoc, inr_normalizationCoprodIso_hom_fromNormalization, inr_normalizationCoprodIso_hom_fromNormalization_assoc, inr_toNormalization_normalizationCoprodIso_inv, inr_toNormalization_normalizationCoprodIso_inv_assoc, instIsAffineHomToNormalization, instIsDominantToNormalization, instIsIntegralHomFromNormalization, instIsIntegralHomNormalizationDesc, instIsIntegralNormalization, instIsIsoNormalizationPullbackOfSmooth, instIsIsoToNormalizationOfIsIntegralHom, instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget, instIsReducedNormalization, instQuasiCompactToNormalization, instQuasiSeparatedToNormalization, ker_toNormalization, hom_ext, normalizationCoprodIso_inv_coprodDesc_fromNormalization, normalizationCoprodIso_inv_coprodDesc_fromNormalization_assoc, normalizationDesc_comp, normalizationDesc_comp_assoc, normalizationObjIso_hom_val, normalizationPullback_snd, normalizationPullback_snd_assoc, preservesLocalization_normalizationDiagramMap, toNormalization_app_preimage, toNormalization_fromNormalization, toNormalization_fromNormalization_assoc, toNormalization_inl_normalizationCoprodIso_hom, toNormalization_inl_normalizationCoprodIso_hom_assoc, toNormalization_inr_normalizationCoprodIso_hom, toNormalization_inr_normalizationCoprodIso_hom_assoc, toNormalization_normalizationDesc, toNormalization_normalizationDesc_assoc, toNormalization_normalizationPullback_fst, toNormalization_normalizationPullback_fst_assoc, ι_fromNormalization, ι_fromNormalization_assoc, ι_toNormalization, ι_toNormalization_assoc	48
Total	60

AlgebraicGeometry.Scheme.Hom

Definitions

Name	Category	Theorems
fromNormalization 📖	CompOp	23 math math: toNormalization_normalizationPullback_fst, normalizationDesc_comp_assoc, toNormalization_fromNormalization_assoc, toNormalization_app_preimage, fromNormalization_preimage, instIsIsoNormalizationPullbackOfSmooth, normalizationPullback_snd_assoc, inl_normalizationCoprodIso_hom_fromNormalization_assoc, inl_normalizationCoprodIso_hom_fromNormalization, inr_normalizationCoprodIso_hom_fromNormalization_assoc, normalizationDesc_comp, instIsIntegralHomFromNormalization, normalizationCoprodIso_inv_coprodDesc_fromNormalization, fromNormalization_app_assoc, ι_fromNormalization_assoc, normalizationCoprodIso_inv_coprodDesc_fromNormalization_assoc, toNormalization_normalizationPullback_fst_assoc, toNormalization_fromNormalization, normalizationPullback_snd, ι_fromNormalization, normalizationObjIso_hom_val, fromNormalization_app, inr_normalizationCoprodIso_hom_fromNormalization
instIsIntegralHomNormalizationPullback 📖	CompOp	—
normalization 📖	CompOp	49 math math: toNormalization_inl_normalizationCoprodIso_hom_assoc, toNormalization_normalizationPullback_fst, inr_toNormalization_normalizationCoprodIso_inv, exists_isIso_morphismRestrict_toNormalization, toNormalization_normalizationDesc, instIsIsoToNormalizationOfIsIntegralHom, toNormalization_inr_normalizationCoprodIso_hom, normalizationDesc_comp_assoc, toNormalization_fromNormalization_assoc, toNormalization_app_preimage, fromNormalization_preimage, ι_toNormalization, AlgebraicGeometry.instIsOpenImmersionCompSchemeιQuasiFiniteLocusToNormalization, AlgebraicGeometry.instIsOpenImmersionToNormalizationOfLocallyQuasiFiniteOfLocallyOfFiniteType, instIsIsoNormalizationPullbackOfSmooth, normalizationPullback_snd_assoc, inl_normalizationCoprodIso_hom_fromNormalization_assoc, inl_normalizationCoprodIso_hom_fromNormalization, instIsIntegralHomNormalizationDesc, inr_normalizationCoprodIso_hom_fromNormalization_assoc, normalizationDesc_comp, instIsIntegralHomFromNormalization, normalizationCoprodIso_inv_coprodDesc_fromNormalization, exists_mem_and_isIso_morphismRestrict_toNormalization, ι_toNormalization_assoc, fromNormalization_app_assoc, ker_toNormalization, toNormalization_inr_normalizationCoprodIso_hom_assoc, instIsReducedNormalization, ι_fromNormalization_assoc, instQuasiSeparatedToNormalization, toNormalization_normalizationDesc_assoc, normalizationCoprodIso_inv_coprodDesc_fromNormalization_assoc, toNormalization_normalizationPullback_fst_assoc, inl_toNormalization_normalizationCoprodIso_inv_assoc, AlgebraicGeometry.instUniversallyClosedToNormalization, toNormalization_fromNormalization, toNormalization_inl_normalizationCoprodIso_hom, inr_toNormalization_normalizationCoprodIso_inv_assoc, normalizationPullback_snd, ι_fromNormalization, normalizationObjIso_hom_val, instQuasiCompactToNormalization, instIsDominantToNormalization, fromNormalization_app, instIsIntegralNormalization, instIsAffineHomToNormalization, inl_toNormalization_normalizationCoprodIso_inv, inr_normalizationCoprodIso_hom_fromNormalization
normalizationCoprodIso 📖	CompOp	14 math math: toNormalization_inl_normalizationCoprodIso_hom_assoc, inr_toNormalization_normalizationCoprodIso_inv, toNormalization_inr_normalizationCoprodIso_hom, inl_normalizationCoprodIso_hom_fromNormalization_assoc, inl_normalizationCoprodIso_hom_fromNormalization, inr_normalizationCoprodIso_hom_fromNormalization_assoc, normalizationCoprodIso_inv_coprodDesc_fromNormalization, toNormalization_inr_normalizationCoprodIso_hom_assoc, normalizationCoprodIso_inv_coprodDesc_fromNormalization_assoc, inl_toNormalization_normalizationCoprodIso_inv_assoc, toNormalization_inl_normalizationCoprodIso_hom, inr_toNormalization_normalizationCoprodIso_inv_assoc, inl_toNormalization_normalizationCoprodIso_inv, inr_normalizationCoprodIso_hom_fromNormalization
normalizationDesc 📖	CompOp	5 math math: toNormalization_normalizationDesc, normalizationDesc_comp_assoc, instIsIntegralHomNormalizationDesc, normalizationDesc_comp, toNormalization_normalizationDesc_assoc
normalizationDiagram 📖	CompOp	4 math math: coequifibered_normalizationDiagramMap, preservesLocalization_normalizationDiagramMap, ι_fromNormalization_assoc, ι_fromNormalization
normalizationDiagramMap 📖	CompOp	4 math math: coequifibered_normalizationDiagramMap, preservesLocalization_normalizationDiagramMap, ι_fromNormalization_assoc, ι_fromNormalization
normalizationGlueData 📖	CompOp	1 math math: instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget
normalizationObjIso 📖	CompOp	4 math math: toNormalization_app_preimage, fromNormalization_app_assoc, normalizationObjIso_hom_val, fromNormalization_app
normalizationOpenCover 📖	CompOp	5 math math: fromNormalization_preimage, ι_toNormalization, ι_toNormalization_assoc, ι_fromNormalization_assoc, ι_fromNormalization
normalizationPullback 📖	CompOp	5 math math: toNormalization_normalizationPullback_fst, instIsIsoNormalizationPullbackOfSmooth, normalizationPullback_snd_assoc, toNormalization_normalizationPullback_fst_assoc, normalizationPullback_snd
toNormalization 📖	CompOp	29 math math: toNormalization_inl_normalizationCoprodIso_hom_assoc, toNormalization_normalizationPullback_fst, inr_toNormalization_normalizationCoprodIso_inv, exists_isIso_morphismRestrict_toNormalization, toNormalization_normalizationDesc, instIsIsoToNormalizationOfIsIntegralHom, toNormalization_inr_normalizationCoprodIso_hom, toNormalization_fromNormalization_assoc, toNormalization_app_preimage, ι_toNormalization, AlgebraicGeometry.instIsOpenImmersionCompSchemeιQuasiFiniteLocusToNormalization, AlgebraicGeometry.instIsOpenImmersionToNormalizationOfLocallyQuasiFiniteOfLocallyOfFiniteType, exists_mem_and_isIso_morphismRestrict_toNormalization, ι_toNormalization_assoc, ker_toNormalization, toNormalization_inr_normalizationCoprodIso_hom_assoc, instQuasiSeparatedToNormalization, toNormalization_normalizationDesc_assoc, toNormalization_normalizationPullback_fst_assoc, inl_toNormalization_normalizationCoprodIso_inv_assoc, AlgebraicGeometry.instUniversallyClosedToNormalization, toNormalization_fromNormalization, toNormalization_inl_normalizationCoprodIso_hom, inr_toNormalization_normalizationCoprodIso_inv_assoc, normalizationObjIso_hom_val, instQuasiCompactToNormalization, instIsDominantToNormalization, instIsAffineHomToNormalization, inl_toNormalization_normalizationCoprodIso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coequifibered_normalizationDiagramMap 📖	mathematical	—	CategoryTheory.NatTrans.Coequifibered Opposite AlgebraicGeometry.Scheme.AffineZariskiSite CommRingCat CategoryTheory.Category.opposite Preorder.smallCategory AlgebraicGeometry.Scheme.AffineZariskiSite.instPreorder CommRingCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.op AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor AlgebraicGeometry.PresheafedSpace.presheaf normalizationDiagram CategoryTheory.Functor.whiskerLeft normalizationDiagramMap	—	AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen_le AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway AlgebraicGeometry.Scheme.basicOpen_le preimage_mono AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen preimage_basicOpen Mathlib.Tactic.DepRewrite.nddcongrArg AlgebraicGeometry.isLocalization_basicOpen_of_qcqs isCompact_preimage AlgebraicGeometry.IsAffineOpen.isCompact isQuasiSeparated_preimage AlgebraicGeometry.IsAffineOpen.isQuasiSeparated IsScalarTower.of_algebraMap_eq' LE.le.trans le_rfl app_eq_appLE map_appLE IsLocalization.Away.integralClosure
fromNormalization_app 📖	mathematical	—	app normalization fromNormalization CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CommRingCat.carrier Opposite.op AlgebraicGeometry.Scheme.Opens CommRingCat.commRing CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring RingHom.toAlgebra CommRingCat.Hom.hom SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toCommRing CommRingCat.ofHom algebraMap Subalgebra.algebra CategoryTheory.Iso.inv normalizationObjIso	—	isIso_app AlgebraicGeometry.Scheme.instIsOpenImmersionF ι_fromNormalization AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso comp_app congr_app CategoryTheory.instIsSplitMonoMap CategoryTheory.instIsSplitMonoOppositeOpOfIsSplitEpi CategoryTheory.IsSplitEpi.of_iso CategoryTheory.instIsIsoEqToHom AlgebraicGeometry.IsAffineOpen.fromSpec_app_self LE.le.trans le_rfl app_eq_appLE CategoryTheory.Category.assoc map_appLE appLE_map appIso_inv_appLE CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.eqToHom_op
fromNormalization_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier 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 normalization AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' fromNormalization app CommRingCat.of CommRingCat.carrier Subalgebra CommRing.toCommSemiring CommRingCat.commRing CommSemiring.toSemiring RingHom.toAlgebra CommRingCat.Hom.hom SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toCommRing CommRingCat.ofHom algebraMap Subalgebra.algebra CategoryTheory.Iso.inv normalizationObjIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fromNormalization_app
fromNormalization_preimage 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder normalization TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' fromNormalization Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens opensRange CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion normalizationOpenCover CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme.instIsOpenImmersionF	—	UnivLE.small UnivLE.self Preorder.subsingleton_hom AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin AlgebraicGeometry.Scheme.IsLocallyDirected.instIsOpenImmersionι AlgebraicGeometry.Scheme.Opens.opensRange_ι AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι
inl_normalizationCoprodIso_hom_fromNormalization 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory normalization AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp CategoryTheory.Limits.coprod AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.coprod.inl CategoryTheory.Iso.hom normalizationCoprodIso fromNormalization	—	AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self instIsIntegralHomFromNormalization CategoryTheory.Limits.coprod.desc_comp normalizationDesc_comp CategoryTheory.Limits.colimit.ι_desc
inl_normalizationCoprodIso_hom_fromNormalization_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory normalization AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp CategoryTheory.Limits.coprod AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.coprod.inl CategoryTheory.Iso.hom normalizationCoprodIso fromNormalization	—	AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_normalizationCoprodIso_hom_fromNormalization
inl_toNormalization_normalizationCoprodIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.coprod normalization AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self toNormalization CategoryTheory.Iso.inv normalizationCoprodIso CategoryTheory.Limits.coprod.inl	—	AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self toNormalization_inl_normalizationCoprodIso_hom_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
inl_toNormalization_normalizationCoprodIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory normalization toNormalization CategoryTheory.Limits.coprod AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Iso.inv normalizationCoprodIso CategoryTheory.Limits.coprod.inl	—	AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_toNormalization_normalizationCoprodIso_inv
inr_normalizationCoprodIso_hom_fromNormalization 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory normalization AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp CategoryTheory.Limits.coprod AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.coprod.inr CategoryTheory.Iso.hom normalizationCoprodIso fromNormalization	—	AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self instIsIntegralHomFromNormalization CategoryTheory.Limits.coprod.desc_comp normalizationDesc_comp CategoryTheory.Limits.colimit.ι_desc
inr_normalizationCoprodIso_hom_fromNormalization_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory normalization AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp CategoryTheory.Limits.coprod AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.coprod.inr CategoryTheory.Iso.hom normalizationCoprodIso fromNormalization	—	AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_normalizationCoprodIso_hom_fromNormalization
inr_toNormalization_normalizationCoprodIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.coprod normalization AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self toNormalization CategoryTheory.Iso.inv normalizationCoprodIso CategoryTheory.Limits.coprod.inr	—	AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self toNormalization_inr_normalizationCoprodIso_hom_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
inr_toNormalization_normalizationCoprodIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory normalization toNormalization CategoryTheory.Limits.coprod AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Iso.inv normalizationCoprodIso CategoryTheory.Limits.coprod.inr	—	AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_toNormalization_normalizationCoprodIso_inv
instIsAffineHomToNormalization 📖	mathematical	—	AlgebraicGeometry.IsAffineHom normalization toNormalization	—	CategoryTheory.MorphismProperty.of_postcomp AlgebraicGeometry.instHasOfPostcompPropertySchemeIsAffineHomIsSeparated AlgebraicGeometry.IsSeparated.of_isAffineHom AlgebraicGeometry.IsIntegralHom.toIsAffineHom instIsIntegralHomFromNormalization toNormalization_fromNormalization
instIsDominantToNormalization 📖	mathematical	—	AlgebraicGeometry.IsDominant normalization toNormalization	—	ker_toNormalization dense_iff_closure_eq TopologicalSpace.Closeds.coe_top support_ker instQuasiCompactToNormalization AlgebraicGeometry.Scheme.IdealSheafData.support_bot
instIsIntegralHomFromNormalization 📖	mathematical	—	AlgebraicGeometry.IsIntegralHom normalization fromNormalization	—	AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top AlgebraicGeometry.HasAffineProperty.instIsZariskiLocalAtTarget AlgebraicGeometry.IsIntegralHom.hasAffineProperty AlgebraicGeometry.iSup_affineOpens_eq_top AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.Scheme.Opens.range_ι fromNormalization_preimage CategoryTheory.MorphismProperty.cancel_left_of_respectsIso CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion CategoryTheory.Iso.isIso_inv CategoryTheory.MorphismProperty.cancel_right_of_respectsIso CategoryTheory.Iso.isIso_hom algebraMap_isIntegral_iff integralClosure.AlgebraIsIntegral CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec CategoryTheory.Category.assoc AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec AlgebraicGeometry.morphismRestrict_ι AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac_assoc ι_fromNormalization AlgebraicGeometry.IsIntegralHom.SpecMap_iff
instIsIntegralHomNormalizationDesc 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	AlgebraicGeometry.IsIntegralHom normalization normalizationDesc	—	normalizationDesc_comp instIsIntegralHomFromNormalization AlgebraicGeometry.IsIntegralHom.of_comp AlgebraicGeometry.IsSeparated.of_isAffineHom AlgebraicGeometry.IsIntegralHom.toIsAffineHom
instIsIntegralNormalization 📖	mathematical	—	AlgebraicGeometry.IsIntegral normalization	—	irreducibleSpace_def Set.image_congr Set.image_univ DenseRange.closure_range denseRange instIsDominantToNormalization IsIrreducible.closure IsIrreducible.image IrreducibleSpace.isIrreducible_univ AlgebraicGeometry.irreducibleSpace_of_isIntegral Continuous.continuousOn continuous AlgebraicGeometry.isIntegral_of_irreducibleSpace_of_isReduced instIsReducedNormalization AlgebraicGeometry.isReduced_of_isIntegral
instIsIsoNormalizationPullbackOfSmooth 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory normalization CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.snd AlgebraicGeometry.instQuasiCompactSndScheme AlgebraicGeometry.instQuasiSeparatedSndScheme fromNormalization normalizationPullback	—	AlgebraicGeometry.IsZariskiLocalAtTarget.of_forall_exists_morphismRestrict AlgebraicGeometry.Scheme.instIsLocalAtTargetIsomorphismsZariskiPrecoverage AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.instQuasiCompactSndScheme AlgebraicGeometry.instQuasiSeparatedSndScheme TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open AlgebraicGeometry.Scheme.isBasis_affineOpens Set.mem_univ isOpen_univ TopologicalSpace.Opens.is_open' AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app AlgebraicGeometry.IsIntegralHom.toIsAffineHom AlgebraicGeometry.IsAffineOpen.preimage AlgebraicGeometry.IsIntegralHom.instSndScheme instIsIntegralHomFromNormalization 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 CategoryTheory.Limits.pullback.condition inf_eq_right AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right AlgebraicGeometry.instFlatOfSmooth AlgebraicGeometry.IsAffineOpen.isCompact AlgebraicGeometry.IsAffineOpen.isQuasiSeparated CategoryTheory.isIso_comp_left_iff app_eq_appLE CategoryTheory.Iso.isIso_hom smooth_appLE isCompact_preimage isQuasiSeparated_preimage CategoryTheory.IsPushout.flip CommRingCat.isPushout_tensorProduct Algebra.to_smulCommClass RingEquiv.map_mul' RingEquiv.map_add' AlgHomClass.toRingHomClass AlgHom.algHomClass CategoryTheory.IsPushout.inr_isoPushout_hom_assoc CategoryTheory.Limits.pushout.inr_desc_assoc CategoryTheory.Category.id_comp CategoryTheory.Limits.colimit.ι_desc Function.Bijective.comp AlgEquiv.bijective TensorProduct.toIntegralClosure_bijective_of_smooth RingHom.Smooth.toAlgebra fromNormalization_app CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id IsScalarTower.right RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass normalizationPullback_snd CategoryTheory.Limits.pushout.hom_ext LE.le.trans CategoryTheory.Limits.colimit.ι_desc_assoc appLE_comp_appLE CategoryTheory.eqToHom_op CategoryTheory.IsPushout.inl_isoPushout_inv_assoc CategoryTheory.Functor.map_isIso CategoryTheory.instIsIsoEqToHom CategoryTheory.Iso.isIso_inv CategoryTheory.inv_eqToHom appLE_map CategoryTheory.IsIso.Iso.inv_inv CategoryTheory.ConcreteCategory.mono_of_injective Subtype.val_injective CategoryTheory.cancel_mono toNormalization_normalizationPullback_fst normalizationObjIso_hom_val appLE.congr_simp comp_preimage preimage_mono Mathlib.Tactic.Reassoc.eq_whisker' CommRingCat.hom_ext RingHom.ext CategoryTheory.IsPushout.inl_isoPushout_hom_assoc CategoryTheory.Limits.pushout.inl_desc_assoc AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass CategoryTheory.IsPushout.inr_isoPushout_inv_assoc AlgHom.comp_algebraMap CategoryTheory.IsIso.comp_isIso CategoryTheory.Limits.pushout.map_isIso CategoryTheory.IsIso.id CategoryTheory.isIso_op
instIsIsoToNormalizationOfIsIntegralHom 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory normalization toNormalization	—	AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover AlgebraicGeometry.Scheme.instIsLocalAtTargetIsomorphismsZariskiPrecoverage AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right opensRange_pullbackFst fromNormalization_preimage toNormalization_fromNormalization AlgebraicGeometry.Scheme.Opens.opensRange_ι AlgebraicGeometry.IsAffineOpen.preimage AlgebraicGeometry.IsIntegralHom.toIsAffineHom CategoryTheory.MorphismProperty.cancel_left_of_respectsIso CategoryTheory.MorphismProperty.RespectsIso.isomorphisms CategoryTheory.Iso.isIso_inv CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom AlgHomClass.toRingHomClass AlgHom.algHomClass CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.Cover.pullbackHom_map AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac_assoc ι_toNormalization AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ_assoc integralClosure_eq_top_iff algebraMap_isIntegral_iff RingHom.algebraMap_toAlgebra AlgebraicGeometry.IsIntegralHom.isIntegral_app
instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget 📖	mathematical	—	CategoryTheory.Functor.IsLocallyDirected CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover Preorder.smallCategory AlgebraicGeometry.Scheme.AffineZariskiSite.instPreorder CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor AlgebraicGeometry.Scheme.AffineZariskiSite.instLocallyDirectedIsOpenImmersionDirectedCover normalizationGlueData AlgebraicGeometry.Scheme.forget	—	AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin Preorder.subsingleton_hom
instIsReducedNormalization 📖	mathematical	—	AlgebraicGeometry.IsReduced normalization	—	isReduced_of_injective RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass Subtype.val_injective AlgebraicGeometry.IsReduced.component_reduced AlgebraicGeometry.instIsReducedSpecOfIsReducedCarrier AlgebraicGeometry.IsReduced.of_openCover
instQuasiCompactToNormalization 📖	mathematical	—	AlgebraicGeometry.QuasiCompact normalization toNormalization	—	CategoryTheory.MorphismProperty.of_postcomp AlgebraicGeometry.instHasOfPostcompPropertySchemeQuasiCompactQuasiSeparated AlgebraicGeometry.IsSeparated.instQuasiSeparated AlgebraicGeometry.IsSeparated.of_isAffineHom AlgebraicGeometry.IsIntegralHom.toIsAffineHom instIsIntegralHomFromNormalization toNormalization_fromNormalization
instQuasiSeparatedToNormalization 📖	mathematical	—	AlgebraicGeometry.QuasiSeparated normalization toNormalization	—	toNormalization_fromNormalization AlgebraicGeometry.QuasiSeparated.of_comp
ker_toNormalization 📖	mathematical	—	ker normalization toNormalization Bot.bot AlgebraicGeometry.Scheme.IdealSheafData OrderBot.toBot Preorder.toLE PartialOrder.toPreorder AlgebraicGeometry.Scheme.IdealSheafData.instPartialOrder AlgebraicGeometry.Scheme.IdealSheafData.instOrderBot	—	AlgebraicGeometry.Scheme.IdealSheafData.ext_of_iSup_eq_top AlgebraicGeometry.IsAffineOpen.preimage AlgebraicGeometry.IsIntegralHom.toIsAffineHom instIsIntegralHomFromNormalization TopologicalSpace.IsOpenCover.comap AlgebraicGeometry.iSup_affineOpens_eq_top RingHom.instRingHomClass ker_apply instQuasiCompactToNormalization RingHom.injective_iff_ker_eq_bot CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CommRingCat.forget_preservesLimits CategoryTheory.MorphismProperty.monomorphisms.eq_1 AlgHomClass.toRingHomClass AlgHom.algHomClass CategoryTheory.eqToHom_op CategoryTheory.MorphismProperty.RespectsIso.monomorphisms CategoryTheory.Iso.isIso_hom CategoryTheory.Functor.map_isIso CategoryTheory.instIsIsoEqToHom Subtype.val_injective
normalizationCoprodIso_inv_coprodDesc_fromNormalization 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory normalization CategoryTheory.Limits.coprod AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Iso.inv normalizationCoprodIso CategoryTheory.Limits.coprod.desc fromNormalization	—	AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self normalizationDesc_comp
normalizationCoprodIso_inv_coprodDesc_fromNormalization_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory normalization CategoryTheory.Limits.coprod AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Iso.inv normalizationCoprodIso CategoryTheory.Limits.coprod.desc fromNormalization	—	AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' normalizationCoprodIso_inv_coprodDesc_fromNormalization
normalizationDesc_comp 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	normalization normalizationDesc fromNormalization	—	CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.colimit.ι_desc_assoc AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin Preorder.subsingleton_hom UnivLE.small UnivLE.self AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase CategoryTheory.Category.assoc le_rfl AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec AlgebraicGeometry.Spec.map_comp_assoc CommRingCat.hom_ext RingHom.ext CommRingCat.comp_apply LE.le.trans appLE_comp_appLE app_eq_appLE appLE.congr_simp
normalizationDesc_comp_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	normalization normalizationDesc fromNormalization	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' normalizationDesc_comp
normalizationObjIso_hom_val 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace normalization 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' fromNormalization CommRingCat.of CommRingCat.carrier Subalgebra CommRing.toCommSemiring CommRingCat.commRing CommSemiring.toSemiring RingHom.toAlgebra CommRingCat.Hom.hom app SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toCommRing CategoryTheory.Iso.hom normalizationObjIso CommRingCat.ofHom AlgHom.toRingHom Subalgebra.toSemiring Subalgebra.algebra Subalgebra.val appLE toNormalization	—	appLE.eq_1 toNormalization_app_preimage CategoryTheory.Category.assoc AlgHomClass.toRingHomClass AlgHom.algHomClass CategoryTheory.eqToHom_op CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
normalizationPullback_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory normalization CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.snd AlgebraicGeometry.instQuasiCompactSndScheme AlgebraicGeometry.instQuasiSeparatedSndScheme fromNormalization normalizationPullback	—	normalizationDesc_comp AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.instQuasiCompactSndScheme AlgebraicGeometry.instQuasiSeparatedSndScheme
normalizationPullback_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory normalization CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.snd AlgebraicGeometry.instQuasiCompactSndScheme AlgebraicGeometry.instQuasiSeparatedSndScheme fromNormalization normalizationPullback	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.instQuasiCompactSndScheme AlgebraicGeometry.instQuasiSeparatedSndScheme CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' normalizationPullback_snd
preservesLocalization_normalizationDiagramMap 📖	mathematical	—	CategoryTheory.NatTrans.Coequifibered Opposite AlgebraicGeometry.Scheme.AffineZariskiSite CommRingCat CategoryTheory.Category.opposite Preorder.smallCategory AlgebraicGeometry.Scheme.AffineZariskiSite.instPreorder CommRingCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.op AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor AlgebraicGeometry.PresheafedSpace.presheaf normalizationDiagram CategoryTheory.Functor.whiskerLeft normalizationDiagramMap	—	coequifibered_normalizationDiagramMap
toNormalization_app_preimage 📖	mathematical	—	app normalization toNormalization CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' fromNormalization Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommRingCat.of CommRingCat.carrier Subalgebra CommRing.toCommSemiring CommRingCat.commRing CommSemiring.toSemiring RingHom.toAlgebra CommRingCat.Hom.hom SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toCommRing CategoryTheory.Iso.hom normalizationObjIso CommRingCat.ofHom AlgHom.toRingHom Subalgebra.toSemiring Subalgebra.algebra Subalgebra.val CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom	—	AlgHomClass.toRingHomClass AlgHom.algHomClass AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι toNormalization_fromNormalization AlgebraicGeometry.Scheme.Opens.ι_preimage_self image_top_eq_opensRange AlgebraicGeometry.Scheme.Opens.opensRange_ι AlgebraicGeometry.Scheme.instIsOpenImmersionF fromNormalization_preimage ι_toNormalization le_rfl LE.le.trans Set.image_subset_iff app_eq_appLE comp_appLE AlgebraicGeometry.Scheme.Opens.ι_appLE appLE_map CategoryTheory.eqToHom_op preimage_image_eq appIso_hom CategoryTheory.Category.assoc naturality_assoc CategoryTheory.eqToHom_unop CategoryTheory.eqToHom_map CategoryTheory.eqToHom_trans CategoryTheory.Functor.map_isIso CategoryTheory.instIsIsoEqToHom CategoryTheory.IsIso.eq_inv_comp CategoryTheory.Functor.map_inv CategoryTheory.inv_eqToHom CategoryTheory.NatTrans.naturality_assoc AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc congr_app
toNormalization_fromNormalization 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory normalization toNormalization fromNormalization	—	AlgebraicGeometry.Scheme.Cover.hom_ext TopologicalSpace.IsOpenCover.comap AlgebraicGeometry.iSup_affineOpens_eq_top ι_toNormalization_assoc ι_fromNormalization AlgebraicGeometry.Spec.map_comp_assoc AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec AlgebraicGeometry.morphismRestrict_ι
toNormalization_fromNormalization_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory normalization toNormalization fromNormalization	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toNormalization_fromNormalization
toNormalization_inl_normalizationCoprodIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory normalization AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp toNormalization CategoryTheory.Limits.coprod AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.coprod.inl CategoryTheory.Iso.hom normalizationCoprodIso	—	AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self instIsIntegralHomFromNormalization CategoryTheory.Limits.colimit.ι_desc toNormalization_normalizationDesc
toNormalization_inl_normalizationCoprodIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory normalization AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp toNormalization CategoryTheory.Limits.coprod AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.coprod.inl CategoryTheory.Iso.hom normalizationCoprodIso	—	AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toNormalization_inl_normalizationCoprodIso_hom
toNormalization_inr_normalizationCoprodIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory normalization AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp toNormalization CategoryTheory.Limits.coprod AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.coprod.inr CategoryTheory.Iso.hom normalizationCoprodIso	—	AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self instIsIntegralHomFromNormalization CategoryTheory.Limits.colimit.ι_desc toNormalization_normalizationDesc
toNormalization_inr_normalizationCoprodIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory normalization AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp toNormalization CategoryTheory.Limits.coprod AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.coprod.inr CategoryTheory.Iso.hom normalizationCoprodIso	—	AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiSeparated_comp AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toNormalization_inr_normalizationCoprodIso_hom
toNormalization_normalizationDesc 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	normalization toNormalization normalizationDesc	—	AlgebraicGeometry.Scheme.Cover.hom_ext TopologicalSpace.IsOpenCover.comap AlgebraicGeometry.iSup_affineOpens_eq_top ι_toNormalization_assoc AlgHomClass.toRingHomClass AlgHom.algHomClass AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin CategoryTheory.Limits.colimit.ι_desc AlgebraicGeometry.IsAffineOpen.preimage AlgebraicGeometry.IsIntegralHom.toIsAffineHom AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE_assoc AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec resLE_comp_ι
toNormalization_normalizationDesc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	normalization toNormalization normalizationDesc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toNormalization_normalizationDesc
toNormalization_normalizationPullback_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.Pullback.instHasPullback normalization CategoryTheory.Limits.pullback.snd AlgebraicGeometry.instQuasiCompactSndScheme AlgebraicGeometry.instQuasiSeparatedSndScheme toNormalization fromNormalization normalizationPullback CategoryTheory.Limits.pullback.fst	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.instQuasiCompactSndScheme AlgebraicGeometry.instQuasiSeparatedSndScheme toNormalization_normalizationDesc_assoc CategoryTheory.Limits.limit.lift_π
toNormalization_normalizationPullback_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.Pullback.instHasPullback normalization CategoryTheory.Limits.pullback.snd AlgebraicGeometry.instQuasiCompactSndScheme AlgebraicGeometry.instQuasiSeparatedSndScheme toNormalization fromNormalization normalizationPullback CategoryTheory.Limits.pullback.fst	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.instQuasiCompactSndScheme AlgebraicGeometry.instQuasiSeparatedSndScheme CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toNormalization_normalizationPullback_fst
ι_fromNormalization 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X normalization CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion normalizationOpenCover CategoryTheory.PreZeroHypercover.f fromNormalization AlgebraicGeometry.Spec 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 normalizationDiagram Opposite.op AlgebraicGeometry.Scheme.Opens Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Spec.map CategoryTheory.NatTrans.app normalizationDiagramMap AlgebraicGeometry.IsAffineOpen.fromSpec	—	CategoryTheory.Limits.colimit.ι_desc AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
ι_fromNormalization_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X normalization CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion normalizationOpenCover CategoryTheory.PreZeroHypercover.f fromNormalization AlgebraicGeometry.Spec 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 Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens AlgebraicGeometry.Spec.map normalizationDiagram CategoryTheory.NatTrans.app normalizationDiagramMap AlgebraicGeometry.IsAffineOpen.fromSpec	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_fromNormalization
ι_toNormalization 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens normalization AlgebraicGeometry.Scheme.Opens.ι toNormalization AlgebraicGeometry.Spec Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens.toSpecΓ CommRingCat.of CommRingCat.carrier AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Subalgebra CommRing.toCommSemiring CommRingCat.commRing CommSemiring.toSemiring RingHom.toAlgebra CommRingCat.Hom.hom app SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toCommRing AlgebraicGeometry.Spec.map CommRingCat.ofHom AlgHom.toRingHom Subalgebra.toSemiring Subalgebra.algebra Subalgebra.val CategoryTheory.PreZeroHypercover.f CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion normalizationOpenCover	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOfLocallyDirected
ι_toNormalization_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens AlgebraicGeometry.Scheme.Opens.ι normalization toNormalization AlgebraicGeometry.Spec Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens.toSpecΓ CommRingCat.of CommRingCat.carrier AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Subalgebra CommRing.toCommSemiring CommRingCat.commRing CommSemiring.toSemiring RingHom.toAlgebra CommRingCat.Hom.hom app SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toCommRing AlgebraicGeometry.Spec.map CommRingCat.ofHom AlgHom.toRingHom Subalgebra.toSemiring Subalgebra.algebra Subalgebra.val CategoryTheory.PreZeroHypercover.f CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion normalizationOpenCover	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_toNormalization

AlgebraicGeometry.Scheme.Hom.normalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Hom.normalization AlgebraicGeometry.Scheme.Hom.toNormalization AlgebraicGeometry.Scheme.Hom.fromNormalization	—	—	AlgebraicGeometry.Scheme.Cover.hom_ext AlgebraicGeometry.IsIntegralHom.toIsAffineHom AlgebraicGeometry.Scheme.Hom.instIsIntegralHomFromNormalization AlgebraicGeometry.IsAffineHom.of_comp AlgebraicGeometry.IsSeparated.of_isAffineHom AlgebraicGeometry.eq_of_SpecMap_comp_eq_of_isAffineOpen Subtype.val_injective AlgebraicGeometry.IsAffineOpen.preimage CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.Hom.ι_fromNormalization AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self AlgebraicGeometry.Scheme.Hom.toNormalization_fromNormalization le_refl AlgHomClass.toRingHomClass AlgHom.algHomClass le_rfl AlgebraicGeometry.Scheme.Hom.comp_appLE AlgebraicGeometry.Scheme.Hom.app_eq_appLE AlgebraicGeometry.Spec.map_comp AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec LE.le.trans CategoryTheory.eqToHom_op AlgebraicGeometry.Scheme.Hom.appLE_map AlgebraicGeometry.Scheme.Hom.map_appLE AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage Eq.ge AlgebraicGeometry.Scheme.Hom.preimage_image_eq AlgebraicGeometry.Scheme.Hom.appIso_hom' AlgebraicGeometry.Scheme.Hom.map_appLE_assoc CategoryTheory.eqToHom_map_comp CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id AlgebraicGeometry.SpecMap_ΓSpecIso_hom AlgebraicGeometry.isAffineOpen_top AlgebraicGeometry.isAffine_Spec AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec_assoc AlgebraicGeometry.IsAffineOpen.fromSpec_top AlgebraicGeometry.Scheme.isoSpec_Spec_inv AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc AlgebraicGeometry.Scheme.Hom.appLE.congr_simp Eq.le

---

← Back to Index