Abelian

📁 Source: Mathlib/AlgebraicGeometry/Group/Abelian.lean

Statistics

Metric	Count
Definitions	0
Theorems instIsClosedImmersionLeftSchemeDiscretePUnitOneOverSpecOf, isCommMonObj_of_isProper_of_geometricallyIntegral, isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed	3
Total	3

AlgebraicGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsClosedImmersionLeftSchemeDiscretePUnitOneOverSpecOf 📖	mathematical	—	IsClosedImmersion CategoryTheory.Comma.left Scheme Scheme.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Spec CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategoryOverScheme CategoryTheory.CommaMorphism.left CategoryTheory.MonObj.one CategoryTheory.GrpObj.toMonObj	—	isClosedImmersion_of_comp_eq_id Unique.instSubsingleton CategoryTheory.Over.w
isCommMonObj_of_isProper_of_geometricallyIntegral 📖	mathematical	—	CategoryTheory.IsCommMonObj CategoryTheory.Over Scheme Scheme.instCategory Spec CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain CategoryTheory.instCategoryOver CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategoryOverScheme instBraidedCategoryOverScheme CategoryTheory.GrpObj.toMonObj	—	Scheme.Pullback.instHasPullback IsProper.instSndScheme CategoryTheory.Limits.hasLimitOfHasLimitsOfShape Scheme.Pullback.instHasPullbacks instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian_1 instGeometricallyIntegralSndScheme Flat.instSndScheme Flat.instOfSubsingletonCarrierCarrierCommRingCatOfIsIntegral Unique.instSubsingleton instIsIntegralSpecOfIsDomainCarrier instIsDomain UniversallyOpen.snd instUniversallyOpenOfIsIntegralOfSubsingletonCarrierCarrierCommRingCat instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian instIsLocallyNoetherianSpecOfIsNoetherianRingCarrier IsDedekindRing.toIsNoetherian IsDedekindDomain.toIsDedekindRing IsPrincipalIdealRing.isDedekindDomain instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule instIsLocallyNoetherianPullbackSchemeOfLocallyOfFiniteType IsProper.toLocallyOfFiniteType isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed AlgebraicClosure.isAlgClosed CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η CategoryTheory.Functor.map_injective instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfQuasiCompact instSurjectiveOfNonemptyOfSubsingletonCarrierCarrierCommRingCat instNonemptyCarrierCarrierCommRingCatSpecOfNontrivialCarrier EuclideanDomain.toNontrivial instQuasiCompactOfIsAffineHom isAffineHom_of_isAffine isAffine_Spec CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Functor.map_mul CategoryTheory.Functor.map_inv' CategoryTheory.MonObj.comp_mul CategoryTheory.Functor.Monoidal.μ_fst CategoryTheory.Functor.Monoidal.μ_snd CategoryTheory.GrpObj.comp_inv CategoryTheory.MonObj.one_eq_one CategoryTheory.MonObj.comp_one CategoryTheory.Functor.map_one
isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed 📖	mathematical	—	CategoryTheory.IsCommMonObj CategoryTheory.Over Scheme Scheme.instCategory Spec CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain CategoryTheory.instCategoryOver CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategoryOverScheme instBraidedCategoryOverScheme CategoryTheory.GrpObj.toMonObj	—	ValuationRing.isLocalRing EuclideanDomain.toNontrivial ValuationRing.toPreValuationRing instIsDomain ValuationRing.of_field isClosed_discrete IsLocallyArtinian.discreteTopology IsArtinianScheme.toIsLocallyArtinian instIsArtinianSchemeSpecOfIsArtinianRingCarrier instIsArtinianOfIsSemisimpleModuleOfFinite IsSemisimpleRing.isSemisimpleModule instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors CategoryTheory.Limits.hasLimitOfHasLimitsOfShape Scheme.Pullback.instHasPullbacks IsProper.instCompScheme IsProper.instFstScheme LocallyOfFiniteType.jacobsonSpace IsProper.toLocallyOfFiniteType instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing instIsJacobsonRingOfKrullDimLEOfNatNat PrimeSpectrum.instKrullDimLEOfNatNat Function.surjective_to_subsingleton Unique.instSubsingleton Surjective.instFstScheme CategoryTheory.Over.w CategoryTheory.Limits.limit.lift_π CategoryTheory.CommaMorphism.w instIsClosedImmersionLeftSchemeDiscretePUnitOneOverSpecOf IsClosedImmersion.of_comp IsProper.toIsSeparated IsProper.of_comp CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η CategoryTheory.Over.OverMorphism.ext Set.image_subset_iff Set.diff_eq_empty Set.not_nonempty_iff_eq_empty nonempty_inter_closedPoints Set.diff_eq_compl_inter Set.image_singleton IsLocallyClosed.inter IsOpen.isLocallyClosed IsClosed.isOpen_compl IsClosed.preimage Scheme.Hom.continuous Scheme.Hom.isClosedMap IsProper.toUniversallyClosed IsProper.instOfIsFinite IsFinite.instOfIsClosedImmersion IsClosed.isLocallyClosed Equiv.surjective Scheme.Pullback.instHasPullback ext_of_apply_closedPoint_eq CategoryTheory.Category.assoc Field.instIsLocalRing CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Over.whiskerRight_left_fst CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Category.id_comp CategoryTheory.Over.whiskerRight_left_snd CategoryTheory.CartesianMonoidalCategory.hom_ext CategoryTheory.CartesianMonoidalCategory.comp_lift CategoryTheory.CartesianMonoidalCategory.whiskerRight_fst CategoryTheory.GrpObj.η_whiskerRight_commutator CategoryTheory.CartesianMonoidalCategory.lift_fst_assoc CategoryTheory.SemiCartesianMonoidalCategory.comp_toUnit_assoc CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unit CategoryTheory.CartesianMonoidalCategory.lift_fst CategoryTheory.CartesianMonoidalCategory.lift_snd exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage CategoryTheory.Limits.pullback.lift_fst Set.Finite.subset Set.finite_singleton Set.Finite.image Scheme.Hom.finite_preimage_singleton instLocallyQuasiFiniteOfIsFinite instQuasiCompactMorphismRestrict quasiCompact_comp Scheme.IdealSheafData.instQuasiCompactSubschemeι instQuasiCompactOfUniversallyClosed Set.ext Set.preimage_comp TopCat.coe_comp Scheme.Hom.comp_base morphismRestrict_ι Set.image_preimage_eq_inter_range Set.range_comp Scheme.Opens.range_ι Scheme.IdealSheafData.range_subschemeι Scheme.Hom.support_ker Set.inter_assoc Set.preimage_inter Set.singleton_inter_of_mem IsClosed.closure_eq IsClosedMap.isClosed_range subset_refl Set.instReflSubset ext_of_apply_eq isReduced_of_isIntegral TopologicalSpace.Opens.isOpen IsOpen.dense IrreducibleSpace.toPreirreducibleSpace irreducibleSpace_of_isIntegral Set.Nonempty.preimage Scheme.Hom.surjective Set.image_congr pointOfClosedPoint_comp subsingleton_image_closure_of_finite_of_isPreirreducible CategoryTheory.Over.tensorHom_left Set.image_univ Scheme.Pullback.range_map IsOpenImmersion.mono IsOpenImmersion.of_isIso CategoryTheory.IsIso.id pointOfClosedPoint_apply Set.Nonempty.image_const range_eq_univ instNonemptyCarrierCarrierCommRingCatSpecOfNontrivialCarrier Set.range_id Set.inter_univ IsIrreducible.isPreirreducible IsIrreducible.image IrreducibleSpace.isIrreducible_univ Continuous.continuousOn Set.preimage_range subset_closure CategoryTheory.Over.whiskerLeft_left_fst CategoryTheory.Over.rightUnitor_inv_left_fst CategoryTheory.Category.comp_id CategoryTheory.CommaMorphism.ext CategoryTheory.Over.tensorObj_ext CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_fst CategoryTheory.GrpObj.whiskerLeft_η_commutator CategoryTheory.Limits.pullback.lift.congr_simp CategoryTheory.Over.whiskerLeft_left_snd CategoryTheory.Over.rightUnitor_inv_left_snd_assoc

---

← Back to Index