Main results 1 to 100
| Declaration | Kind | Where | Note |
|---|---|---|---|
AlgebraicGeometry.Scheme.Hom.exists_isFinite_morphismRestrict_of_discreteTopology_genericPoints |
theorem | SchemeProperties/GenericFiniteness/Components.lean, line 84 | |
AlgebraicGeometry.Scheme.Hom.exists_isFinite_morphismRestrict_of_finite_irreducibleComponents |
theorem | SchemeProperties/GenericFiniteness/Components.lean, line 160 | |
PrimeSpectrum.isReduced_atPrime_homeomorphOfRingEquiv_iff |
theorem | SchemeProperties/ReducedLocusEquiv.lean, line 34 | |
PrimeSpectrum.isOpen_isReduced_atPrime_iff_ringEquiv |
theorem | SchemeProperties/ReducedLocusEquiv.lean, line 53 | |
MvPolynomial.isOpen_reduced_atPrime_pointSquareZeroQuotient_iff_finite_range |
theorem | SchemeProperties/PolynomialPointSquareZeroReducedLocus.lean, line 45 | |
CategoryTheory.Subfunctor.IsOneCoverDense |
def | SchemeProperties/SingleCoverExtension.lean, line 55 | |
CategoryTheory.Subfunctor.oneCoverExtensionEquiv |
def | SchemeProperties/SingleCoverExtension.lean, line 252 | |
CategoryTheory.Subfunctor.IsOneCoverDense.grpObj |
def | SchemeProperties/SingleCoverGroup.lean, line 404 | |
CategoryTheory.Subfunctor.IsOneCoverDense.grpObj_isMonHom |
theorem | SchemeProperties/SingleCoverGroup.lean, line 635 | |
CategoryTheory.Subfunctor.IsOneCoverDense.grpObj_unique |
theorem | SchemeProperties/SingleCoverGroup.lean, line 646 | |
CategoryTheory.Subfunctor.extendOneCoverIso |
def | SchemeProperties/SingleCoverExtension.lean, line 365 | |
AlgebraicGeometry.algebraicOverPoints_isSheafFor_faithfullyFlat |
theorem | SchemeProperties/FiniteTypeSingleCover.lean, line 150 | |
AlgebraicGeometry.algebraicOverOneCoverEquiv |
def | SchemeProperties/FiniteTypeSingleCover.lean, line 216 | |
AlgebraicGeometry.extendAlgebraicOverIso |
def | SchemeProperties/FiniteTypeSingleCover.lean, line 275 | |
AlgebraicGeometry.powerImage_isOneCoverDense |
theorem | SchemeProperties/PowerImage.lean, line 191 | |
AlgebraicGeometry.laurentUnit_not_mem_powerImage |
theorem | SchemeProperties/PowerImage.lean, line 239 | |
AlgebraicGeometry.powerImage_not_isSheafFor_root |
theorem | SchemeProperties/PowerImage.lean, line 292 | |
AlgebraicGeometry.zeroAdditiveSubfunctor_not_oneCoverDense |
theorem | SchemeProperties/PowerImage.lean, line 309 | |
SheafOfModules.Presentation.isFinite_map |
theorem | SchemeProperties/SheafFinitePresentationTransport.lean, line 43 | |
SheafOfModules.Presentation.isFinitePresentation |
theorem | SchemeProperties/SheafFinitePresentationTransport.lean, line 68 | |
AlgebraicGeometry.Scheme.Modules.isFinite_presentationRestrict |
theorem | SchemeProperties/ModuleFinitePresentation.lean, line 49 | |
AlgebraicGeometry.isFinitePresentation_tilde |
theorem | SchemeProperties/ModuleFinitePresentation.lean, line 77 | |
AlgebraicGeometry.Scheme.Modules.exists_isOpenCover_isFinite_presentation |
theorem | SchemeProperties/ModuleFinitePresentation.lean, line 96 | |
AlgebraicGeometry.Scheme.PartialMap.isOver_comp_of_isDominant_first |
theorem | SchemeProperties/RationalMapComposition.lean, line 34 | |
AlgebraicGeometry.Scheme.RationalMap.isOver_comp_of_isDominant_first |
theorem | SchemeProperties/RationalMapComposition.lean, line 62 | |
AlgebraicGeometry.Scheme.PartialMap.PullsDenseOpens |
def | SchemeProperties/DenseOpenPullback.lean, line 30 | |
AlgebraicGeometry.Scheme.PartialMap.pullsDenseOpens_iff_of_equiv |
theorem | SchemeProperties/DenseOpenPullback.lean, line 41 | |
AlgebraicGeometry.Scheme.PartialMap.pullsDenseOpens_restrict_iff |
theorem | SchemeProperties/DenseOpenPullback.lean, line 67 | |
AlgebraicGeometry.Scheme.PartialMap.pullsDenseOpens_of_isOpenMap |
theorem | SchemeProperties/DenseOpenPullback.lean, line 73 | |
AlgebraicGeometry.Scheme.PartialMap.pullsDenseOpens_of_isDominant |
theorem | SchemeProperties/DenseOpenPullback.lean, line 82 | |
AlgebraicGeometry.Scheme.RationalMap.PullsDenseOpens |
def | SchemeProperties/DenseOpenPullback.lean, line 94 | |
AlgebraicGeometry.Scheme.PartialMap.pullsDenseOpens_toRationalMap_iff |
theorem | SchemeProperties/DenseOpenPullback.lean, line 102 | |
AlgebraicGeometry.Scheme.RationalMap.pullsDenseOpens_representative_iff |
theorem | SchemeProperties/DenseOpenPullback.lean, line 115 | |
AlgebraicGeometry.Scheme.PartialMap.compOfPullsDenseOpens |
def | SchemeProperties/DenseOpenComposition.lean, line 42 | |
AlgebraicGeometry.Scheme.RationalMap.compOfPullsDenseOpens |
def | SchemeProperties/DenseOpenComposition.lean, line 141 | |
AlgebraicGeometry.Scheme.PartialMap.compOfPullsDenseOpens_equiv_of_equiv |
theorem | SchemeProperties/DenseOpenComposition.lean, line 108 | |
AlgebraicGeometry.Scheme.RationalMap.toRationalMap_compOfPullsDenseOpens |
theorem | SchemeProperties/DenseOpenComposition.lean, line 157 | |
AlgebraicGeometry.Scheme.PartialMap.compOfPullsDenseOpens_toPartialMap |
theorem | SchemeProperties/DenseOpenComposition.lean, line 119 | |
AlgebraicGeometry.Scheme.RationalMap.compOfPullsDenseOpens_toRationalMap |
theorem | SchemeProperties/DenseOpenComposition.lean, line 169 | |
AlgebraicGeometry.Scheme.PartialMap.compOfPullsDenseOpens_eq_comp |
theorem | SchemeProperties/DenseOpenComposition.lean, line 129 | |
AlgebraicGeometry.Scheme.RationalMap.compOfPullsDenseOpens_eq_comp |
theorem | SchemeProperties/DenseOpenComposition.lean, line 177 | |
AlgebraicGeometry.Scheme.PartialMap.isOver_compOfPullsDenseOpens |
theorem | SchemeProperties/DenseOpenCompositionOver.lean, line 46 | |
AlgebraicGeometry.Scheme.RationalMap.isOver_compOfPullsDenseOpens |
theorem | SchemeProperties/DenseOpenCompositionOver.lean, line 75 | |
AlgebraicGeometry.Scheme.PartialMap.pullsDenseOpens_compOfPullsDenseOpens |
theorem | SchemeProperties/DenseOpenCompositionClosure.lean, line 51 | |
AlgebraicGeometry.Scheme.RationalMap.pullsDenseOpens_compOfPullsDenseOpens |
theorem | SchemeProperties/DenseOpenCompositionClosure.lean, line 63 | |
AlgebraicGeometry.Scheme.PartialMap.compOfPullsDenseOpens_assoc |
theorem | SchemeProperties/DenseOpenCompositionAssociativity.lean, line 43 | |
AlgebraicGeometry.Scheme.RationalMap.compOfPullsDenseOpens_assoc |
theorem | SchemeProperties/DenseOpenCompositionAssociativity.lean, line 65 | |
AlgebraicGeometry.Scheme.PartialMap.pullsDenseOpens_id |
theorem | SchemeProperties/DenseOpenCompositionUnits.lean, line 43 | |
AlgebraicGeometry.Scheme.PartialMap.id_compOfPullsDenseOpens |
theorem | SchemeProperties/DenseOpenCompositionUnits.lean, line 52 | |
AlgebraicGeometry.Scheme.PartialMap.compOfPullsDenseOpens_id |
theorem | SchemeProperties/DenseOpenCompositionUnits.lean, line 66 | |
AlgebraicGeometry.Scheme.RationalMap.pullsDenseOpens_id |
theorem | SchemeProperties/DenseOpenCompositionUnits.lean, line 76 | |
AlgebraicGeometry.Scheme.RationalMap.id_compOfPullsDenseOpens |
theorem | SchemeProperties/DenseOpenCompositionUnits.lean, line 80 | |
AlgebraicGeometry.Scheme.RationalMap.compOfPullsDenseOpens_id |
theorem | SchemeProperties/DenseOpenCompositionUnits.lean, line 90 | |
AlgebraicGeometry.Scheme.PartialMap.isDominant_of_pullsDenseOpens |
theorem | SchemeProperties/DenseOpenPullbackDominance.lean, line 31 | |
AlgebraicGeometry.Scheme.PartialMap.pullsDenseOpens_iff_isDominant |
theorem | SchemeProperties/DenseOpenPullbackDominance.lean, line 43 | |
AlgebraicGeometry.Scheme.RationalMap.isDominant_of_pullsDenseOpens |
theorem | SchemeProperties/DenseOpenPullbackDominance.lean, line 56 | |
AlgebraicGeometry.Scheme.RationalMap.pullsDenseOpens_iff_isDominant |
theorem | SchemeProperties/DenseOpenPullbackDominance.lean, line 64 | |
AlgebraicGeometry.DenseOpenRationalScheme |
structure | SchemeProperties/DenseOpenRationalCategory.lean, line 30 | |
AlgebraicGeometry.DenseOpenRationalScheme.of |
def | SchemeProperties/DenseOpenRationalCategory.lean, line 37 | |
AlgebraicGeometry.DenseOpenRationalScheme.Hom |
structure | SchemeProperties/DenseOpenRationalCategory.lean, line 40 | |
AlgebraicGeometry.DenseOpenRationalScheme.hom |
def | SchemeProperties/DenseOpenRationalCategory.lean, line 46 | |
AlgebraicGeometry.DenseOpenRationalScheme.toRationalMap_hom |
theorem | SchemeProperties/DenseOpenRationalCategory.lean, line 49 | |
AlgebraicGeometry.DenseOpenRationalScheme.hom_ext |
theorem | SchemeProperties/DenseOpenRationalCategory.lean, line 54 | |
AlgebraicGeometry.DenseOpenRationalScheme.toRationalMap_id |
theorem | SchemeProperties/DenseOpenRationalCategory.lean, line 76 | |
AlgebraicGeometry.DenseOpenRationalScheme.toRationalMap_comp |
theorem | SchemeProperties/DenseOpenRationalCategory.lean, line 79 | |
AlgebraicGeometry.DenseOpenRationalScheme.homEquivDominant |
def | SchemeProperties/DenseOpenRationalCategory.lean, line 87 | |
AlgebraicGeometry.DenseOpenRationalScheme.homEquivDominant_apply_val |
theorem | SchemeProperties/DenseOpenRationalCategory.lean, line 103 | |
AlgebraicGeometry.IntegralDominantRationalScheme |
structure | SchemeProperties/IntegralDominantRationalCategory.lean, line 69 | |
AlgebraicGeometry.IntegralDominantRationalScheme.Hom |
structure | SchemeProperties/IntegralDominantRationalCategory.lean, line 84 | |
AlgebraicGeometry.IntegralDominantRationalScheme.toRationalMap_id |
theorem | SchemeProperties/IntegralDominantRationalCategory.lean, line 120 | |
AlgebraicGeometry.IntegralDominantRationalScheme.toRationalMap_comp |
theorem | SchemeProperties/IntegralDominantRationalCategory.lean, line 123 | |
AlgebraicGeometry.IntegralDenseOpenRationalScheme |
abbrev | SchemeProperties/IntegralDominantRationalCategory.lean, line 36 | |
AlgebraicGeometry.IntegralDenseOpenRationalScheme.toNative |
def | SchemeProperties/IntegralDominantRationalCategory.lean, line 145 | |
AlgebraicGeometry.IntegralDominantRationalScheme.toDenseOpen |
def | SchemeProperties/IntegralDominantRationalCategory.lean, line 186 | |
AlgebraicGeometry.integralDenseOpenEquivalence |
def | SchemeProperties/IntegralDominantRationalCategory.lean, line 235 | |
AlgebraicGeometry.DenseOpenRationalSchemeOver |
structure | SchemeProperties/DenseOpenRationalCategoryOver.lean, line 30 | |
AlgebraicGeometry.DenseOpenRationalSchemeOver.of |
def | SchemeProperties/DenseOpenRationalCategoryOver.lean, line 39 | |
AlgebraicGeometry.DenseOpenRationalSchemeOver.Hom |
structure | SchemeProperties/DenseOpenRationalCategoryOver.lean, line 50 | |
AlgebraicGeometry.DenseOpenRationalSchemeOver.hom |
def | SchemeProperties/DenseOpenRationalCategoryOver.lean, line 59 | |
AlgebraicGeometry.DenseOpenRationalSchemeOver.toRationalMap_hom |
theorem | SchemeProperties/DenseOpenRationalCategoryOver.lean, line 64 | |
AlgebraicGeometry.DenseOpenRationalSchemeOver.isOver_iff_compHom |
theorem | SchemeProperties/DenseOpenRationalCategoryOver.lean, line 73 | |
AlgebraicGeometry.DenseOpenRationalSchemeOver.hom_ext |
theorem | SchemeProperties/DenseOpenRationalCategoryOver.lean, line 87 | |
AlgebraicGeometry.DenseOpenRationalSchemeOver.toRationalMap_id |
theorem | SchemeProperties/DenseOpenRationalCategoryOver.lean, line 121 | |
AlgebraicGeometry.DenseOpenRationalSchemeOver.toRationalMap_comp |
theorem | SchemeProperties/DenseOpenRationalCategoryOver.lean, line 124 | |
AlgebraicGeometry.DenseOpenRationalSchemeOver.forget |
def | SchemeProperties/DenseOpenRationalCategoryOver.lean, line 131 | |
AlgebraicGeometry.DenseOpenRationalSchemeOver.forget_obj_toScheme |
theorem | SchemeProperties/DenseOpenRationalCategoryOver.lean, line 137 | |
AlgebraicGeometry.DenseOpenRationalSchemeOver.forget_map_toRationalMap |
theorem | SchemeProperties/DenseOpenRationalCategoryOver.lean, line 140 | |
AlgebraicGeometry.IntegralDenseOpenRationalSchemeOver |
abbrev | SchemeProperties/IntegralDominantRationalCategoryOver.lean, line 35 | |
AlgebraicGeometry.IntegralDominantRationalSchemeOver |
structure | SchemeProperties/IntegralDominantRationalCategoryOver.lean, line 68 | |
AlgebraicGeometry.IntegralDominantRationalSchemeOver.Hom |
structure | SchemeProperties/IntegralDominantRationalCategoryOver.lean, line 86 | |
AlgebraicGeometry.IntegralDominantRationalSchemeOver.isOver_iff_compHom |
theorem | SchemeProperties/IntegralDominantRationalCategoryOver.lean, line 116 | |
AlgebraicGeometry.IntegralDenseOpenRationalSchemeOver.toNative |
def | SchemeProperties/IntegralDominantRationalCategoryOver.lean, line 183 | |
AlgebraicGeometry.IntegralDominantRationalSchemeOver.toDenseOpen |
def | SchemeProperties/IntegralDominantRationalCategoryOver.lean, line 222 | |
AlgebraicGeometry.integralDenseOpenEquivalenceOver |
def | SchemeProperties/IntegralDominantRationalCategoryOver.lean, line 270 | |
AlgebraicGeometry.IntegralDenseOpenRationalSchemeOver.forget |
def | SchemeProperties/IntegralDominantRationalCategoryOver.lean, line 284 | |
AlgebraicGeometry.IntegralDominantRationalSchemeOver.forget |
def | SchemeProperties/IntegralDominantRationalCategoryOver.lean, line 320 | |
AlgebraicGeometry.IntegralDenseOpenRationalSchemeOver.forgetInclusionIso |
def | SchemeProperties/IntegralDominantRationalCategoryOver.lean, line 346 | |
AlgebraicGeometry.IntegralDenseOpenRationalSchemeOver.forgetNativeIso |
def | SchemeProperties/IntegralDominantRationalCategoryOver.lean, line 359 | |
AlgebraicGeometry.IntegralDominantRationalSchemeOver.forgetDenseOpenIso |
def | SchemeProperties/IntegralDominantRationalCategoryOver.lean, line 386 | |
AlgebraicGeometry.Scheme.RationalMap.fromFunctionField_closedPoint |
theorem | SchemeProperties/RationalFunctionFieldPullback.lean, line 74 |
Quoted from the main results in formalization.yaml of FormalFrontier/scheme-properties at commit 09db7d88, Apache-2.0.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.