Section4

📁 Source: Hochster/Section4.lean

Statistics

Metric	Count
Definitions ISupExtForV, IndExtForV, MemClosurePairs, z, isIndex, iSupExtForV, repPoly, «termσ(_)»»)	8
Theorems eq_iUnion_indExtForV, mono_of_isIndex_of_isIndex, subset_of_le, apply_ne_zero_of_pi_valuation_of_v_extension_of_map_apply_eq, map_apply_le_of_pi_valuation_of_v_extension, map_div_apply_mul_map_apply_of_pi_valuation_of_forall_imp, map_div_apply_of_pi_valuation, map_mul_apply_of_pi_valuation, map_zpow_apply_of_pi_valuation, mem_closure, constantCoeff_repPoly_apply_eq_zero_of_apply_eq_zero_of_apply_eq_zero, constantCoeff_repPoly_apply_ne_zero_of_apply_eq_zero_of_apply_ne_zero, div_mul_cancel_of_forall_imp, mul_pow_mem_of_mem_closure_insert_div_of_natDegree_repPoly_le, mul_pow_natDegree_repPoly_apply_eq_zero_of_apply_eq_zero, mul_pow_natDegree_repPoly_apply_ne_zero_of_apply_ne_zero_of_apply_ne_zero, polynomial_eval_apply, polynomial_eval_apply', support_eq_inter_union_inter_of_mem_closure_insert_div, vanishing_set_eq_inter_union_inter_of_mem_closure_insert_div, vanishing_set_eq_inter_union_inter_of_mem_closure_insert_div₁, isCompact_support_of_mem_closure_insert_div, isCompact_vanishing_set_of_mem_closure_insert_div, closureInsertDiv, closureInsertDiv_isIndex_of_forall_map_apply_le_of_forall_ne_zero, exists_isIndex_iff_exists_isIndex_of_subset, exists_isIndex_of_forall_exist_eq_and_mem_and_mem_and_forall_imp_and_exists_isIndex, exists_isIndex_of_forall_springLike'_closure_insert_div_of_forall_isIndex, exists_le_map_apply_of_mem_closure_insert_div, exists_springLike'_closure_union_isIndex, exists_springLike'_iSupExtForV_isIndex, exists_springLike'_indExtForV_isIndex, false_of_apply_eq_zero_of_apply_ne_zero, forall_exists_le, forall_exists_of_ne_zero, forall_iff_of_ne, forall_le_of_ne, forall_map_apply_le_and_forall_apply_ne_zero_iff_exists_isIndex, iSupExtForV_isIndex, indExtForV, indExtForV_isIndex, isClosed_vanishing_set_of_forall_map_apply_le_of_forall_ne_zero, map_apply_eq_one_iff_apply_ne_zero_of_forall_map_apply_le_of_forall_ne_zero, map_apply_le_of_apply_ne_zero_of_map_apply_ne_one, map_apply_le_one_of_mem_closure_insert_div_of_forall_map_apply_le, mem_radical_span_singleton_of_forall_imp, support_is_patch_of_mem_closure_insert_div, vanishing_set_is_patch_of_mem_closure_insert_div, coeff_repPoly_mem, exists_finset_subset_and_mem_closure_union_of_mem_closure_union, exists_polynomial_of_mem_closure, exists_polynomial_of_mem_closure₁, repPoly_eval_eq, apply_le_generator_of_apply_lt_one, isClosed_iff_forall_closure_subset_of_isClosed_constructibleTop, mem_iSupExtForV_iff	56
Total	64

ISupExtForV

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_iUnion_indExtForV 📖	mathematical	—	ISupExtForV IndExtForV	—	IndExtForV.subset_of_le

IndExtForV

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono_of_isIndex_of_isIndex 📖	mathematical	SpringLike' SpringLike'.isIndex	IndExtForV	—	SpringLike'.isIndex.exists_springLike'_indExtForV_isIndex SpringLike'.isIndex.exists_isIndex_iff_exists_isIndex_of_subset
subset_of_le 📖	mathematical	—	IndExtForV	—	—

MemClosurePairs

Definitions

Name	Category	Theorems
z 📖	CompOp	25 math math: SWICat.valuationFun_apply_lt_iff_forall_prod_lt_of_ne_zero, SpringLike'.isIndex.forall_le_of_ne, SpringLike'.isIndex.forall_iff_of_ne, SpringLike'.isIndex.forall_exists_of_ne_zero, SpringLike'.isIndex.map_apply_le_of_apply_ne_zero_of_map_apply_ne_one, map_apply_le_of_pi_valuation_of_v_extension, SWICat.prod_le_valuationFun_apply_of_mem_support, SWICat.evalMapApplyPoly_ne_zero_iff_valuationFun_apply_evalMapApplyPoly_eq_one, SWICat.valuationFun_apply_of_support_nonempty, map_mul_apply_of_pi_valuation, SWICat.valuationFun_apply_eq_iff_of_support_nonempty, SWICat.v_apply_ringHomToPiFractionRing_apply', map_div_apply_mul_map_apply_of_pi_valuation_of_forall_imp, map_zpow_apply_of_pi_valuation, map_div_apply_of_pi_valuation, SWICat.valuationFun_apply_X, SWICat.valuationFun_apply_monomial, SpringLike'.isIndex.exists_le_map_apply_of_mem_closure_insert_div, SWICat.v_apply_ringHomToPiFractionRing_apply, SWICat.valuationFun_apply_le_iff_forall_prod_le, SpringLike'.isIndex.forall_map_apply_le_and_forall_apply_ne_zero_iff_exists_isIndex, SWICat.valuationFun_apply_eq_iff_of_ne_zero, SWICat.valuationFun_apply_lt_iff_forall_prod_lt_of_support_nonempty, SpringLike'.isIndex.forall_exists_le, mem_closure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_ne_zero_of_pi_valuation_of_v_extension_of_map_apply_eq 📖	—	SpringLike' SpringLike'.isIndex z	—	—	SpringLike'.isIndex.forall_iff_of_ne
map_apply_le_of_pi_valuation_of_v_extension 📖	mathematical	SpringLike' SpringLike'.isIndex	z	—	SpringLike'.isIndex.forall_le_of_ne map_mul_apply_of_pi_valuation Pi.div_mul_cancel_of_forall_imp
map_div_apply_mul_map_apply_of_pi_valuation_of_forall_imp 📖	mathematical	—	z	—	Pi.div_mul_cancel_of_forall_imp map_mul_apply_of_pi_valuation
map_div_apply_of_pi_valuation 📖	mathematical	—	z	—	—
map_mul_apply_of_pi_valuation 📖	mathematical	—	z	—	—
map_zpow_apply_of_pi_valuation 📖	mathematical	—	z	—	—
mem_closure 📖	mathematical	—	z	—	—

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
constantCoeff_repPoly_apply_eq_zero_of_apply_eq_zero_of_apply_eq_zero 📖	mathematical	—	Subring.repPoly	—	Subring.repPoly_eval_eq polynomial_eval_apply
constantCoeff_repPoly_apply_ne_zero_of_apply_eq_zero_of_apply_ne_zero 📖	—	—	—	—	Subring.repPoly_eval_eq polynomial_eval_apply
div_mul_cancel_of_forall_imp 📖	—	—	—	—	—
mul_pow_mem_of_mem_closure_insert_div_of_natDegree_repPoly_le 📖	—	Subring.repPoly	—	—	Subring.repPoly_eval_eq Subring.coeff_repPoly_mem div_mul_cancel_of_forall_imp
mul_pow_natDegree_repPoly_apply_eq_zero_of_apply_eq_zero 📖	mathematical	—	Subring.repPoly	—	—
mul_pow_natDegree_repPoly_apply_ne_zero_of_apply_ne_zero_of_apply_ne_zero 📖	—	—	—	—	—
polynomial_eval_apply 📖	—	—	—	—	—
polynomial_eval_apply' 📖	—	—	—	—	—
support_eq_inter_union_inter_of_mem_closure_insert_div 📖	mathematical	—	Subring.repPoly	—	constantCoeff_repPoly_apply_ne_zero_of_apply_eq_zero_of_apply_ne_zero mul_pow_natDegree_repPoly_apply_ne_zero_of_apply_ne_zero_of_apply_ne_zero polynomial_eval_apply Subring.repPoly_eval_eq
vanishing_set_eq_inter_union_inter_of_mem_closure_insert_div 📖	mathematical	—	Subring.repPoly	—	constantCoeff_repPoly_apply_eq_zero_of_apply_eq_zero_of_apply_eq_zero mul_pow_natDegree_repPoly_apply_eq_zero_of_apply_eq_zero polynomial_eval_apply Subring.repPoly_eval_eq
vanishing_set_eq_inter_union_inter_of_mem_closure_insert_div₁ 📖	mathematical	—	Subring.repPoly	—	constantCoeff_repPoly_apply_eq_zero_of_apply_eq_zero_of_apply_eq_zero mul_pow_natDegree_repPoly_apply_eq_zero_of_apply_eq_zero polynomial_eval_apply Subring.repPoly_eval_eq

SpringLike'

Definitions

Name	Category	Theorems
isIndex 📖	CompData	1 math math: SWICat.springLike'_mapRingHomToPiFractionRing_isIndex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact_support_of_mem_closure_insert_div 📖	—	SpringLike'	—	—	compactSpace_of_isEmbedding_of_isClosed_constructibleTop_range spectralSpace support_is_patch_of_mem_closure_insert_div
isCompact_vanishing_set_of_mem_closure_insert_div 📖	—	SpringLike'	—	—	compactSpace_of_isEmbedding_of_isClosed_constructibleTop_range spectralSpace vanishing_set_is_patch_of_mem_closure_insert_div
support_is_patch_of_mem_closure_insert_div 📖	mathematical	SpringLike'	ConstructibleTop ConstructibleTop.instTopologicalSpace	—	forall_isOpen Pi.mul_pow_mem_of_mem_closure_insert_div_of_natDegree_repPoly_le forall_isCompact Subring.coeff_repPoly_mem Pi.support_eq_inter_union_inter_of_mem_closure_insert_div ConstructibleTop.instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image spectralSpace
vanishing_set_is_patch_of_mem_closure_insert_div 📖	mathematical	SpringLike'	ConstructibleTop ConstructibleTop.instTopologicalSpace	—	forall_isOpen Pi.mul_pow_mem_of_mem_closure_insert_div_of_natDegree_repPoly_le forall_isCompact Subring.coeff_repPoly_mem Pi.vanishing_set_eq_inter_union_inter_of_mem_closure_insert_div ConstructibleTop.instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image spectralSpace

SpringLike'.isIndex

Definitions

Name	Category	Theorems
iSupExtForV 📖	CompOp	2 math math: iSupExtForV_springLike_spring_isAffine_of_isSimple, iSupExtForV_isIndex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closureInsertDiv 📖	—	SpringLike' SpringLike'.isIndex MemClosurePairs.z	—	—	SpringLike'.closureUnion isClosed_vanishing_set_of_forall_map_apply_le_of_forall_ne_zero SpringLike'.isCompact_support_of_mem_closure_insert_div
closureInsertDiv_isIndex_of_forall_map_apply_le_of_forall_ne_zero 📖	mathematical	SpringLike' SpringLike'.isIndex MemClosurePairs.z	closureInsertDiv	—	closureInsertDiv forall_exists_of_ne_zero map_apply_le_one_of_mem_closure_insert_div_of_forall_map_apply_le map_apply_eq_one_iff_apply_ne_zero_of_forall_map_apply_le_of_forall_ne_zero exists_le_map_apply_of_mem_closure_insert_div
exists_isIndex_iff_exists_isIndex_of_subset 📖	—	SpringLike' SpringLike'.isIndex	—	—	forall_map_apply_le_and_forall_apply_ne_zero_iff_exists_isIndex
exists_isIndex_of_forall_exist_eq_and_mem_and_mem_and_forall_imp_and_exists_isIndex 📖	—	SpringLike' SpringLike'.isIndex	—	—	exists_isIndex_of_forall_springLike'_closure_insert_div_of_forall_isIndex
exists_isIndex_of_forall_springLike'_closure_insert_div_of_forall_isIndex 📖	—	SpringLike' SpringLike'.isIndex	—	—	SpringLike'.congr_simp congr_simp forall_map_apply_le_and_forall_apply_ne_zero_iff_exists_isIndex
exists_le_map_apply_of_mem_closure_insert_div 📖	mathematical	SpringLike' SpringLike'.isIndex	MemClosurePairs.z	—	forall_exists_le Subring.coeff_repPoly_mem Pi.mul_pow_mem_of_mem_closure_insert_div_of_natDegree_repPoly_le Subring.repPoly_eval_eq Pi.polynomial_eval_apply' forall_le_of_ne
exists_springLike'_closure_union_isIndex 📖	—	SpringLike' SpringLike'.isIndex	—	—	SpringLike'.spectralSpace SpringLike'.forall_isOpen SpringLike'.forall_isCompact SpringLike'.isTopologicalBasis forall_exists_of_ne_zero forall_le_of_ne forall_iff_of_ne forall_exists_le exists_isIndex_of_forall_exist_eq_and_mem_and_mem_and_forall_imp_and_exists_isIndex Subring.exists_finset_subset_and_mem_closure_union_of_mem_closure_union
exists_springLike'_iSupExtForV_isIndex 📖	mathematical	SpringLike' SpringLike'.isIndex	ISupExtForV	—	SpringLike'.spectralSpace SpringLike'.forall_isOpen SpringLike'.forall_isCompact SpringLike'.isTopologicalBasis mem_iSupExtForV_iff forall_exists_of_ne_zero forall_le_of_ne forall_iff_of_ne forall_exists_le exists_springLike'_indExtForV_isIndex
exists_springLike'_indExtForV_isIndex 📖	mathematical	SpringLike' SpringLike'.isIndex	IndExtForV	—	exists_springLike'_closure_union_isIndex
false_of_apply_eq_zero_of_apply_ne_zero 📖	—	SpringLike' SpringLike'.isIndex MemClosurePairs.z	—	—	forall_iff_of_ne
forall_exists_le 📖	mathematical	SpringLike' SpringLike'.isIndex	MemClosurePairs.z	—	—
forall_exists_of_ne_zero 📖	mathematical	SpringLike' SpringLike'.isIndex	MemClosurePairs.z	—	—
forall_iff_of_ne 📖	mathematical	SpringLike' SpringLike'.isIndex	MemClosurePairs.z	—	—
forall_le_of_ne 📖	mathematical	SpringLike' SpringLike'.isIndex	MemClosurePairs.z	—	—
forall_map_apply_le_and_forall_apply_ne_zero_iff_exists_isIndex 📖	mathematical	SpringLike' SpringLike'.isIndex	MemClosurePairs.z	—	closureInsertDiv closureInsertDiv_isIndex_of_forall_map_apply_le_of_forall_ne_zero MemClosurePairs.map_apply_le_of_pi_valuation_of_v_extension MemClosurePairs.apply_ne_zero_of_pi_valuation_of_v_extension_of_map_apply_eq
iSupExtForV_isIndex 📖	mathematical	SpringLike' SpringLike'.isIndex	ISupExtForV iSupExtForV	—	exists_springLike'_iSupExtForV_isIndex
indExtForV 📖	mathematical	SpringLike' SpringLike'.isIndex	IndExtForV	—	exists_springLike'_indExtForV_isIndex
indExtForV_isIndex 📖	mathematical	SpringLike' SpringLike'.isIndex	IndExtForV indExtForV	—	exists_springLike'_indExtForV_isIndex
isClosed_vanishing_set_of_forall_map_apply_le_of_forall_ne_zero 📖	—	SpringLike' SpringLike'.isIndex MemClosurePairs.z	—	—	isClosed_iff_forall_closure_subset_of_isClosed_constructibleTop SpringLike'.spectralSpace SpringLike'.vanishing_set_is_patch_of_mem_closure_insert_div SpringLike'.forall_isOpen Subring.coeff_repPoly_mem Pi.constantCoeff_repPoly_apply_eq_zero_of_apply_eq_zero_of_apply_eq_zero Pi.vanishing_set_eq_inter_union_inter_of_mem_closure_insert_div Subring.repPoly_eval_eq Pi.polynomial_eval_apply' forall_le_of_ne Pi.vanishing_set_eq_inter_union_inter_of_mem_closure_insert_div₁ forall_iff_of_ne Pi.mul_pow_mem_of_mem_closure_insert_div_of_natDegree_repPoly_le Pi.mul_pow_natDegree_repPoly_apply_eq_zero_of_apply_eq_zero
map_apply_eq_one_iff_apply_ne_zero_of_forall_map_apply_le_of_forall_ne_zero 📖	—	SpringLike' SpringLike'.isIndex MemClosurePairs.z	—	—	Pi.support_eq_inter_union_inter_of_mem_closure_insert_div forall_iff_of_ne forall_le_of_ne Pi.mul_pow_mem_of_mem_closure_insert_div_of_natDegree_repPoly_le Subring.coeff_repPoly_mem Pi.polynomial_eval_apply Subring.repPoly_eval_eq Pi.polynomial_eval_apply' false_of_apply_eq_zero_of_apply_ne_zero SpringLike'.forall_isOpen MemClosurePairs.mem_closure
map_apply_le_of_apply_ne_zero_of_map_apply_ne_one 📖	mathematical	SpringLike' SpringLike'.isIndex	MemClosurePairs.z	—	forall_exists_of_ne_zero forall_le_of_ne
map_apply_le_one_of_mem_closure_insert_div_of_forall_map_apply_le 📖	—	SpringLike' SpringLike'.isIndex MemClosurePairs.z	—	—	Pi.support_eq_inter_union_inter_of_mem_closure_insert_div forall_le_of_ne Subring.coeff_repPoly_mem Pi.polynomial_eval_apply Subring.repPoly_eval_eq
mem_radical_span_singleton_of_forall_imp 📖	—	SpringLike' SpringLike'.isIndex ISupExtForV	—	—	mem_iSupExtForV_iff IndExtForV.subset_of_le exists_springLike'_indExtForV_isIndex forall_exists_le map_apply_le_of_apply_ne_zero_of_map_apply_ne_one forall_le_of_ne forall_map_apply_le_and_forall_apply_ne_zero_iff_exists_isIndex forall_iff_of_ne Pi.div_mul_cancel_of_forall_imp

Subring

Definitions

Name	Category	Theorems
repPoly 📖	CompOp	7 math math: Pi.vanishing_set_eq_inter_union_inter_of_mem_closure_insert_div₁, Pi.vanishing_set_eq_inter_union_inter_of_mem_closure_insert_div, Pi.mul_pow_natDegree_repPoly_apply_eq_zero_of_apply_eq_zero, Pi.constantCoeff_repPoly_apply_eq_zero_of_apply_eq_zero_of_apply_eq_zero, coeff_repPoly_mem, repPoly_eval_eq, Pi.support_eq_inter_union_inter_of_mem_closure_insert_div

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_repPoly_mem 📖	mathematical	—	repPoly	—	exists_polynomial_of_mem_closure
exists_finset_subset_and_mem_closure_union_of_mem_closure_union 📖	—	—	—	—	—
exists_polynomial_of_mem_closure 📖	—	—	—	—	—
exists_polynomial_of_mem_closure₁ 📖	—	—	—	—	Set.insert.eq_1 exists_polynomial_of_mem_closure
repPoly_eval_eq 📖	mathematical	—	repPoly	—	exists_polynomial_of_mem_closure

Valuation.IsRankOneDiscrete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_le_generator_of_apply_lt_one 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
ISupExtForV 📖	CompOp	5 math math: SpringLike'.isIndex.iSupExtForV_springLike_spring_isAffine_of_isSimple, ISupExtForV.eq_iUnion_indExtForV, mem_iSupExtForV_iff, SpringLike'.isIndex.exists_springLike'_iSupExtForV_isIndex, SpringLike'.isIndex.iSupExtForV_isIndex
IndExtForV 📖	CompOp	10 math math: SpringLike'.isIndex.indExtForVIsSimple_h, ISupExtForV.eq_iUnion_indExtForV, SpringLike'.isIndex.indExtForVIsSimple_h', mem_iSupExtForV_iff, SpringLike'.isIndex.indExtForV_isIndex, IndExtForV.subset_of_le, IndExtForV.mono_of_isIndex_of_isIndex, SpringLike'.isIndex.exists_springLike'_indExtForV_isIndex, SpringLike'.isIndex.indExtForVIsSimple_f, SpringLike'.isIndex.indExtForV
MemClosurePairs 📖	CompData	—
«termσ(_)» 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed_iff_forall_closure_subset_of_isClosed_constructibleTop 📖	—	—	—	—	mem_patch_closure_iff_mem_pt_closure
mem_iSupExtForV_iff 📖	mathematical	—	ISupExtForV IndExtForV	—	IndExtForV.subset_of_le

---

← Back to Index