Documentation Verification Report

Section3

📁 Source: Hochster/Section3.lean

Statistics

Metric	Count
Definitions `ringHomToPiFractionRing`, `SpringCat`, `A`, `Hom`, `comp`, `hom'`, `id`, `X`, `commRing`, `f`, `inclusionRingHom`, `instCategory`, `isAffine`, `homeomorph`, `springLike`, `tX`, `SpringLike`, `SpringLike'`, `springLike`, `homeomorph`, `forall_commRing`, `h`, `i`, `matchingIdeal`, `spring`, `homeomorph`	26
Theorems `isReduced_of_forall_isReduced`, `ringHomToPiFractionRing_apply`, `ringHomToPiFractionRing_apply_eq_zero_iff_of_forall_isDomain`, `ringHomToPiFractionRing_apply_ne_zero_iff_of_forall_isDomain`, `ringHomToPiFractionRing_injective_of_forall_isDomain`, `isTopologicalBasis_inter_biInter`, `zeroLocus_singleton`, `ext`, `ext_iff`, `image_subset`, `ext`, `ext_iff`, `inclusionRingHom_injective`, `instSpectralSpaceX`, `isAffine_iff_forall_mem_radical_of_subset`, `isEmbedding`, `isReduced`, `isSpectralMap`, `range_dense`, `range_isClosed`, `springLike'`, `springLike_matchingIdeal`, `springLike_spring_cancel`, `springLike_spring_f`, `closureUnion`, `forall_isCompact`, `forall_isOpen`, `isReduced`, `isTopologicalBasis`, `mapRingHomToPiFractionRing`, `spectralSpace`, `springLike_spring_isAffine_iff_forall_mem_radical_of_subset`, `forall_isCompact`, `forall_isDomain`, `forall_isOpen`, `fun_matchingIdeal_injective`, `injective`, `isEmbedding_fun_matchingIdeal`, `isReduced`, `isSpectralMap_fun_matchingIdeal`, `isTopologicalBasis`, `matchingIdeal_isPrime`, `mem_matchingIdeal_iff_eq_zero`, `spectralSpace`, `springLike'`, `spring_isAffine_iff_forall_mem_radical_of_subset`, `exists_mem_compl_of_isClosed_of_ne_univ`, `eq_of_isTopologicalBasis_of_isTopologicalBasis`	48
Total	74

Pi

Definitions

Name	Category	Theorems
`ringHomToPiFractionRing` 📖	CompOp	7 math math: `ringHomToPiFractionRing_apply`, `SWICat.v_apply_ringHomToPiFractionRing_apply'`, `ringHomToPiFractionRing_injective_of_forall_isDomain`, `SpringLike'.mapRingHomToPiFractionRing`, `SWICat.springLike'_mapRingHomToPiFractionRing_isIndex`, `SWICat.v_apply_ringHomToPiFractionRing_apply`, `ringHomToPiFractionRing_apply_eq_zero_iff_of_forall_isDomain`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isReduced_of_forall_isReduced` 📖	—	—	—	—	—
`ringHomToPiFractionRing_apply` 📖	mathematical	—	`ringHomToPiFractionRing`	—	—
`ringHomToPiFractionRing_apply_eq_zero_iff_of_forall_isDomain` 📖	mathematical	—	`ringHomToPiFractionRing`	—	—
`ringHomToPiFractionRing_apply_ne_zero_iff_of_forall_isDomain` 📖	—	—	—	—	`ringHomToPiFractionRing_apply_eq_zero_iff_of_forall_isDomain`
`ringHomToPiFractionRing_injective_of_forall_isDomain` 📖	mathematical	—	`ringHomToPiFractionRing`	—	—

PrimeSpectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`zeroLocus_singleton` 📖	—	—	—	—	—

PrimeSpectrum.ConstructibleTop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTopologicalBasis_inter_biInter` 📖	mathematical	—	`ConstructibleTop` `ConstructibleTop.instTopologicalSpace`	—	`PrimeSpectrum.zeroLocus_singleton` `ConstructibleTop.instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image`

SpringCat

Definitions

Name	Category	Theorems
`A` 📖	CompOp	13 math math: `isReduced`, `isSpectralMap`, `isAffine_iff_forall_mem_radical_of_subset`, `springLike_spring_cancel`, `springLike'`, `range_dense`, `Hom.image_subset`, `ext_iff`, `springLike_spring_f`, `inclusionRingHom_injective`, `isEmbedding`, `range_isClosed`, `springLike_matchingIdeal`
`Hom` 📖	CompData	—
`X` 📖	CompOp	12 math math: `isSpectralMap`, `springLike_spring_cancel`, `springLike'`, `range_dense`, `Hom.image_subset`, `ext_iff`, `springLike_spring_f`, `inclusionRingHom_injective`, `instSpectralSpaceX`, `isEmbedding`, `range_isClosed`, `springLike_matchingIdeal`
`commRing` 📖	CompOp	13 math math: `isReduced`, `isSpectralMap`, `isAffine_iff_forall_mem_radical_of_subset`, `springLike_spring_cancel`, `springLike'`, `range_dense`, `Hom.image_subset`, `ext_iff`, `springLike_spring_f`, `inclusionRingHom_injective`, `isEmbedding`, `range_isClosed`, `springLike_matchingIdeal`
`f` 📖	CompOp	10 math math: `isSpectralMap`, `springLike'`, `range_dense`, `Hom.image_subset`, `ext_iff`, `springLike_spring_f`, `inclusionRingHom_injective`, `isEmbedding`, `range_isClosed`, `springLike_matchingIdeal`
`inclusionRingHom` 📖	CompOp	2 math math: `springLike'`, `inclusionRingHom_injective`
`instCategory` 📖	CompOp	—
`isAffine` 📖	MathDef	5 math math: `SpringLike'.isIndex.iSupExtForV_springLike_spring_isAffine_of_isSimple`, `SpringLike'.springLike_spring_isAffine_iff_forall_mem_radical_of_subset`, `SpringLike.spring_isAffine_iff_forall_mem_radical_of_subset`, `isAffine_iff_forall_mem_radical_of_subset`, `SpringLike'.springLike_spring_isAffine_of_isSimple_of_forall_imp`
`springLike` 📖	CompOp	3 math math: `springLike_spring_cancel`, `springLike_spring_f`, `springLike_matchingIdeal`
`tX` 📖	CompOp	8 math math: `isSpectralMap`, `springLike_spring_cancel`, `springLike'`, `ext_iff`, `springLike_spring_f`, `instSpectralSpaceX`, `isEmbedding`, `springLike_matchingIdeal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`X` `tX` `A` `commRing` `f`	—	—	—
`ext_iff` 📖	mathematical	—	`X` `tX` `A` `commRing` `f`	—	`ext`
`inclusionRingHom_injective` 📖	mathematical	—	`A` `commRing` `X` `f` `inclusionRingHom`	—	`isReduced` `range_dense`
`instSpectralSpaceX` 📖	mathematical	—	`X` `tX`	—	`spectralSpace_of_isEmbedding_of_isClosed_constructibleTop_range` `isEmbedding` `range_isClosed`
`isAffine_iff_forall_mem_radical_of_subset` 📖	mathematical	—	`isAffine` `A` `commRing`	—	`springLike_spring_cancel` `springLike_matchingIdeal` `SpringLike.spring_isAffine_iff_forall_mem_radical_of_subset`
`isEmbedding` 📖	mathematical	—	`X` `A` `commRing` `tX` `f`	—	—
`isReduced` 📖	mathematical	—	`A` `commRing`	—	—
`isSpectralMap` 📖	mathematical	—	`X` `A` `commRing` `tX` `f`	—	`spectralSpace_and_isSpectralMap_iff_isClosed_constructibleTop_range` `isEmbedding` `range_isClosed`
`range_dense` 📖	mathematical	—	`A` `commRing` `X` `f`	—	—
`range_isClosed` 📖	mathematical	—	`ConstructibleTop` `A` `commRing` `ConstructibleTop.instTopologicalSpace` `X` `f`	—	—
`springLike'` 📖	mathematical	—	`SpringLike'` `X` `tX` `A` `commRing` `f` `inclusionRingHom`	—	`instSpectralSpaceX` `SpringLike.forall_isOpen` `SpringLike.forall_isCompact` `SpringLike.isTopologicalBasis`
`springLike_matchingIdeal` 📖	mathematical	—	`SpringLike.matchingIdeal` `X` `A` `tX` `commRing` `springLike` `f`	—	`springLike_spring_f`
`springLike_spring_cancel` 📖	mathematical	—	`SpringLike.spring` `X` `A` `tX` `commRing` `springLike`	—	`ext` `springLike_spring_f`
`springLike_spring_f` 📖	mathematical	—	`f` `SpringLike.spring` `X` `A` `tX` `commRing` `springLike`	—	`inclusionRingHom_injective`

SpringCat.Hom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	—
`hom'` 📖	CompOp	2 math math: `image_subset`, `ext_iff`
`id` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`hom'`	—	—	—
`ext_iff` 📖	mathematical	—	`hom'`	—	`ext`
`image_subset` 📖	mathematical	—	`SpringCat.A` `SpringCat.commRing` `hom'` `SpringCat.X` `SpringCat.f`	—	—

SpringCat.isAffine

Definitions

Name	Category	Theorems
`homeomorph` 📖	CompOp	—

SpringLike

Definitions

Name	Category	Theorems
`forall_commRing` 📖	CompOp	7 math math: `springLike'`, `forall_isCompact`, `forall_isDomain`, `mem_matchingIdeal_iff_eq_zero`, `forall_isOpen`, `isTopologicalBasis`, `injective`
`h` 📖	CompOp	6 math math: `springLike'`, `forall_isCompact`, `mem_matchingIdeal_iff_eq_zero`, `forall_isOpen`, `isTopologicalBasis`, `injective`
`i` 📖	CompOp	7 math math: `springLike'`, `forall_isCompact`, `forall_isDomain`, `mem_matchingIdeal_iff_eq_zero`, `forall_isOpen`, `isTopologicalBasis`, `injective`
`matchingIdeal` 📖	CompOp	6 math math: `isSpectralMap_fun_matchingIdeal`, `isEmbedding_fun_matchingIdeal`, `mem_matchingIdeal_iff_eq_zero`, `matchingIdeal_isPrime`, `fun_matchingIdeal_injective`, `SpringCat.springLike_matchingIdeal`
`spring` 📖	CompOp	6 math math: `SpringLike'.isIndex.iSupExtForV_springLike_spring_isAffine_of_isSimple`, `SpringLike'.springLike_spring_isAffine_iff_forall_mem_radical_of_subset`, `spring_isAffine_iff_forall_mem_radical_of_subset`, `SpringCat.springLike_spring_cancel`, `SpringCat.springLike_spring_f`, `SpringLike'.springLike_spring_isAffine_of_isSimple_of_forall_imp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forall_isCompact` 📖	mathematical	—	`i` `forall_commRing` `h`	—	—
`forall_isDomain` 📖	mathematical	—	`i` `forall_commRing`	—	—
`forall_isOpen` 📖	mathematical	—	`i` `forall_commRing` `h`	—	—
`fun_matchingIdeal_injective` 📖	mathematical	—	`matchingIdeal`	—	`spectralSpace` `isTopologicalBasis`
`injective` 📖	mathematical	—	`i` `forall_commRing` `h`	—	—
`isEmbedding_fun_matchingIdeal` 📖	mathematical	—	`matchingIdeal` `matchingIdeal_isPrime`	—	`matchingIdeal_isPrime` `TopologicalSpace.eq_of_isTopologicalBasis_of_isTopologicalBasis` `isTopologicalBasis` `fun_matchingIdeal_injective`
`isReduced` 📖	—	—	—	—	`injective` `Pi.isReduced_of_forall_isReduced` `forall_isDomain`
`isSpectralMap_fun_matchingIdeal` 📖	mathematical	—	`matchingIdeal` `matchingIdeal_isPrime`	—	`matchingIdeal_isPrime` `isEmbedding_fun_matchingIdeal` `forall_isCompact`
`isTopologicalBasis` 📖	mathematical	—	`i` `forall_commRing` `h`	—	—
`matchingIdeal_isPrime` 📖	mathematical	—	`matchingIdeal`	—	`forall_isDomain`
`mem_matchingIdeal_iff_eq_zero` 📖	mathematical	—	`matchingIdeal` `i` `forall_commRing` `h`	—	—
`spectralSpace` 📖	—	—	—	—	—
`springLike'` 📖	mathematical	—	`SpringLike'` `i` `forall_commRing` `forall_isDomain` `h`	—	`forall_isDomain` `spectralSpace` `forall_isOpen` `forall_isCompact` `isTopologicalBasis`
`spring_isAffine_iff_forall_mem_radical_of_subset` 📖	mathematical	—	`SpringCat.isAffine` `spring`	—	`mem_matchingIdeal_iff_eq_zero` `matchingIdeal_isPrime` `TopologicalSpace.IsTopologicalBasis.exists_mem_compl_of_isClosed_of_ne_univ` `PrimeSpectrum.ConstructibleTop.isTopologicalBasis_inter_biInter` `SpringCat.range_isClosed`

SpringLike'

Definitions

Name	Category	Theorems
`springLike` 📖	CompOp	3 math math: `isIndex.iSupExtForV_springLike_spring_isAffine_of_isSimple`, `springLike_spring_isAffine_iff_forall_mem_radical_of_subset`, `springLike_spring_isAffine_of_isSimple_of_forall_imp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closureUnion` 📖	—	`SpringLike'`	—	—	`spectralSpace` `isTopologicalBasis`
`forall_isCompact` 📖	—	`SpringLike'`	—	—	—
`forall_isOpen` 📖	—	`SpringLike'`	—	—	—
`isReduced` 📖	—	`SpringLike'`	—	—	`SpringLike.isReduced`
`isTopologicalBasis` 📖	—	`SpringLike'`	—	—	—
`mapRingHomToPiFractionRing` 📖	mathematical	`SpringLike'`	`Pi.ringHomToPiFractionRing`	—	`spectralSpace` `forall_isOpen` `forall_isCompact` `isTopologicalBasis` `Pi.ringHomToPiFractionRing_apply_ne_zero_iff_of_forall_isDomain`
`spectralSpace` 📖	—	`SpringLike'`	—	—	—
`springLike_spring_isAffine_iff_forall_mem_radical_of_subset` 📖	mathematical	`SpringLike'`	`SpringCat.isAffine` `SpringLike.spring` `springLike`	—	`SpringLike.spring_isAffine_iff_forall_mem_radical_of_subset`

SpringLike'.springLike.spring.isAffine

Definitions

Name	Category	Theorems
`homeomorph` 📖	CompOp	—

SpringLike.spring.isAffine

Definitions

Name	Category	Theorems
`homeomorph` 📖	CompOp	—

TopologicalSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_isTopologicalBasis_of_isTopologicalBasis` 📖	—	—	—	—	—

TopologicalSpace.IsTopologicalBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_compl_of_isClosed_of_ne_univ` 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
`SpringCat` 📖	CompData	—
`SpringLike` 📖	CompData	—
`SpringLike'` 📖	CompData	3 math math: `SpringLike.springLike'`, `SpringCat.springLike'`, `SWICat.springLike'`

---

← Back to Index