Documentation Verification Report

Module

📁 Source: FLT/Patching/Module.lean

Statistics

Metric	Count
Definitions `IsPatchingSystem`, `linearMap`, `UniformlyBoundedRank`, `bound`, `linearMap`, `rank`, `OpenIdeals`, `PatchingModule`, `Component`, `componentMap`, `componentMapModule`, `constEquiv`, `equivComponent`, `incl`, `liftComponent`, `map`, `mapEquiv`, `mapOfIsPatchingSystem`, `ofPi`, `submodule`, `toConst`, `π`, `instAddCommGroupPatchingModule`, `instModuleForallPatchingModule`, `instModulePatchingModule`, `instOrderTopOpenIdeals`, `instSemilatticeInfOpenIdeals`, `instTopologicalSpacePatchingModule`	28
Theorems `cond`, `linearMap_bijective`, `linearMap_compLeft`, `card_quotient_le`, `cond`, `exists_finsupp_surjective`, `exists_rank`, `finite_quotient_smul`, `finrank_lt_bound`, `linearMap_eq_zero`, `linearMap_surjective`, `rank_lt_bound`, `rank_spec`, `componentMapModule_surjective`, `continuous_ofPi`, `incl_apply`, `isClosed_submodule`, `mapEquiv_apply`, `mapEquiv_symm_apply`, `mapOfIsPatchingSystem_bijective`, `map_apply`, `map_comp`, `map_comp_apply`, `map_id`, `map_surjective`, `ofPi_apply`, `ofPi_surjective`, `rank_patchingModule`, `smul_apply`, `toConst_surjective`, `instContinuousSMulComponentValIdealIsOpenCoe`, `instContinuousSMulPatchingModule`, `instFiniteComponentValIdealIsOpenCoeOfUniformlyBoundedRankOfFreeQuotientAnnihilator`, `instFinitePatchingModule`, `instFiniteQuotientIdealAnnihilator_fLT`, `instFinite_fLT`, `instFreePatchingModule`, `instIsScalarTowerForallPatchingModule`, `instIsTopologicalAddGroupPatchingModule`, `instT2SpacePatchingModule`, `instTotallyDisconnectedSpacePatchingModule`	41
Total	69

IsPatchingSystem

Definitions

Name	Category	Theorems
`linearMap` 📖	CompOp	2 math math: `linearMap_compLeft`, `linearMap_bijective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cond` 📖	—	—	—	—	—
`linearMap_bijective` 📖	mathematical	—	`Module.UniformlyBoundedRank.rank` `linearMap`	—	`cond` `Module.UniformlyBoundedRank.linearMap_eq_zero` `Module.UniformlyBoundedRank.linearMap_surjective` `Pi.liftQuotientₗ_bijective`
`linearMap_compLeft` 📖	mathematical	—	`Module.UniformlyBoundedRank.rank` `linearMap` `Module.UniformlyBoundedRank.linearMap`	—	—

Module

Definitions

Name	Category	Theorems
`UniformlyBoundedRank` 📖	CompData	—

Module.UniformlyBoundedRank

Definitions

Name	Category	Theorems
`bound` 📖	CompOp	5 math math: `exists_finsupp_surjective`, `card_quotient_le`, `finrank_lt_bound`, `rank_lt_bound`, `maximalIdeal_pow_bound_le_smul_top`
`linearMap` 📖	CompOp	2 math math: `IsPatchingSystem.linearMap_compLeft`, `linearMap_surjective`
`rank` 📖	CompOp	7 math math: `PatchingModule.mapOfIsPatchingSystem_bijective`, `PatchingModule.continuous_ofPi`, `IsPatchingSystem.linearMap_compLeft`, `IsPatchingSystem.linearMap_bijective`, `PatchingModule.rank_patchingModule`, `linearMap_surjective`, `rank_spec`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_quotient_le` 📖	mathematical	—	`bound`	—	`exists_finsupp_surjective` `Pi.liftQuotientₗ_surjective`
`cond` 📖	—	—	—	—	—
`exists_finsupp_surjective` 📖	mathematical	—	`bound`	—	`instFiniteQuotientIdealAnnihilator_fLT` `finrank_lt_bound`
`exists_rank` 📖	—	—	—	—	`rank_lt_bound` `instFiniteQuotientIdealAnnihilator_fLT`
`finite_quotient_smul` 📖	—	—	—	—	`exists_finsupp_surjective` `Pi.liftQuotientₗ_surjective`
`finrank_lt_bound` 📖	mathematical	—	`bound`	—	`rank_lt_bound`
`linearMap_eq_zero` 📖	—	—	—	—	`rank_spec` `linearMap.eq_1`
`linearMap_surjective` 📖	mathematical	—	`rank` `linearMap`	—	`rank_spec` `linearMap.eq_1`
`rank_lt_bound` 📖	mathematical	—	`bound`	—	`cond`
`rank_spec` 📖	mathematical	—	`rank`	—	`exists_rank`

PatchingModule

Definitions

Name	Category	Theorems
`Component` 📖	CompOp	13 math math: `instFiniteComponentValIdealIsOpenCoeOfUniformlyBoundedRankOfFreeQuotientAnnihilator`, `mapEquiv_apply`, `ofPi_surjective`, `componentMapModule_surjective`, `ofPi_apply`, `instSubsingletonComponentTopIdeal`, `smul_apply`, `incl_apply`, `ker_componentMapModule_mkQ`, `instContinuousSMulComponentValIdealIsOpenCoe`, `isClosed_submodule`, `map_apply`, `mem_smul_top`
`componentMap` 📖	CompOp	—
`componentMapModule` 📖	CompOp	4 math math: `mapEquiv_apply`, `componentMapModule_surjective`, `ker_componentMapModule_mkQ`, `map_apply`
`constEquiv` 📖	CompOp	1 math math: `smul_lemma₁`
`equivComponent` 📖	CompOp	—
`incl` 📖	CompOp	1 math math: `incl_apply`
`liftComponent` 📖	CompOp	—
`map` 📖	CompOp	8 math math: `map_surjective`, `mapEquiv_symm_apply`, `map_id`, `smul_lemma₀`, `map_comp_apply`, `map_comp`, `map_apply`, `ker_map_mkQ`
`mapEquiv` 📖	CompOp	2 math math: `mapEquiv_apply`, `mapEquiv_symm_apply`
`mapOfIsPatchingSystem` 📖	CompOp	2 math math: `mapOfIsPatchingSystem_bijective`, `continuous_ofPi`
`ofPi` 📖	CompOp	2 math math: `ofPi_surjective`, `ofPi_apply`
`submodule` 📖	CompOp	6 math math: `mapEquiv_apply`, `smul_apply`, `incl_apply`, `isClosed_submodule`, `map_apply`, `mem_smul_top`
`toConst` 📖	CompOp	1 math math: `toConst_surjective`
`π` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`componentMapModule_surjective` 📖	mathematical	—	`Component` `instAddCommGroupUltraProduct` `instModuleForallUltraProduct` `componentMapModule`	—	`UltraProduct.map_surjective`
`continuous_ofPi` 📖	mathematical	—	`PatchingModule` `Module.UniformlyBoundedRank.rank` `instTopologicalSpacePatchingModule` `instAddCommGroupPatchingModule` `instModulePatchingModule` `mapOfIsPatchingSystem`	—	—
`incl_apply` 📖	mathematical	—	`OpenIdeals` `Component` `instAddCommGroupUltraProduct` `instModuleForallUltraProduct` `submodule` `PatchingModule` `instAddCommGroupPatchingModule` `instModuleForallPatchingModule` `incl` `UltraProduct` `UltraProduct.πₗ`	—	—
`isClosed_submodule` 📖	mathematical	—	`OpenIdeals` `Component` `instTopologicalSpaceUltraProduct` `instAddCommGroupUltraProduct` `instModuleForallUltraProduct` `submodule`	—	`instDiscreteTopologyUltraProduct`
`mapEquiv_apply` 📖	mathematical	—	`PatchingModule` `instAddCommGroupPatchingModule` `instModuleForallPatchingModule` `mapEquiv` `OpenIdeals` `Component` `instAddCommGroupUltraProduct` `instModuleForallUltraProduct` `submodule` `LinearMap.piMap` `componentMapModule`	—	—
`mapEquiv_symm_apply` 📖	mathematical	—	`PatchingModule` `instAddCommGroupPatchingModule` `instModuleForallPatchingModule` `mapEquiv` `map`	—	—
`mapOfIsPatchingSystem_bijective` 📖	mathematical	—	`PatchingModule` `Module.UniformlyBoundedRank.rank` `instAddCommGroupPatchingModule` `instModulePatchingModule` `mapOfIsPatchingSystem`	—	`exists_ideal_isOpen_and_subset` `denseRange_inverseLimit` `instDiscreteTopologyUltraProduct` `instT2SpacePatchingModule` `continuous_ofPi`
`map_apply` 📖	mathematical	—	`OpenIdeals` `Component` `instAddCommGroupUltraProduct` `instModuleForallUltraProduct` `submodule` `PatchingModule` `instAddCommGroupPatchingModule` `instModuleForallPatchingModule` `map` `componentMapModule`	—	—
`map_comp` 📖	mathematical	—	`map` `PatchingModule` `instAddCommGroupPatchingModule` `instModuleForallPatchingModule`	—	`map_comp_apply`
`map_comp_apply` 📖	mathematical	—	`PatchingModule` `instAddCommGroupPatchingModule` `instModuleForallPatchingModule` `map`	—	`ofPi_surjective`
`map_id` 📖	mathematical	—	`map` `PatchingModule` `instAddCommGroupPatchingModule` `instModuleForallPatchingModule`	—	`UltraProduct.πₗ_surjective`
`map_surjective` 📖	mathematical	—	`PatchingModule` `instAddCommGroupPatchingModule` `instModuleForallPatchingModule` `map`	—	`UltraProduct.πₗ_surjective` `componentMapModule_surjective` `nonempty_inverseLimit_of_finite` `IsLocalRing.isOpen_maximalIdeal_pow''` `instFiniteComponentValIdealIsOpenCoeOfUniformlyBoundedRankOfFreeQuotientAnnihilator`
`ofPi_apply` 📖	mathematical	—	`OpenIdeals` `Component` `instAddCommGroupUltraProduct` `instModuleForallUltraProduct` `ofPi` `UltraProduct` `UltraProduct.πₗ`	—	—
`ofPi_surjective` 📖	mathematical	—	`OpenIdeals` `Component` `instAddCommGroupUltraProduct` `instModuleForallUltraProduct` `ofPi`	—	`UltraProduct.πₗ_surjective`
`rank_patchingModule` 📖	mathematical	—	`PatchingModule` `instAddCommGroupPatchingModule` `instModulePatchingModule` `Module.UniformlyBoundedRank.rank`	—	`mapOfIsPatchingSystem_bijective`
`smul_apply` 📖	mathematical	—	`OpenIdeals` `Component` `instAddCommGroupUltraProduct` `instModuleForallUltraProduct` `submodule` `PatchingModule` `instAddCommGroupPatchingModule` `instModulePatchingModule` `instModuleUltraProduct`	—	—
`toConst_surjective` 📖	mathematical	—	`PatchingModule` `instAddCommGroupPatchingModule` `instModulePatchingModule` `toConst`	—	`IsModuleTopology.compactSpace` `instIsTopologicalAddGroupPatchingModule` `instContinuousSMulPatchingModule` `denseRange_inverseLimit` `instDiscreteTopologyUltraProduct` `UltraProduct.surjective_of_eventually_surjective` `instT2SpacePatchingModule`

(root)

Definitions

Name	Category	Theorems
`IsPatchingSystem` 📖	CompData	—
`OpenIdeals` 📖	CompOp	9 math math: `PatchingAlgebra.smulData.f_mono`, `PatchingModule.mapEquiv_apply`, `PatchingModule.ofPi_surjective`, `PatchingModule.ofPi_apply`, `PatchingModule.smul_apply`, `PatchingModule.incl_apply`, `PatchingModule.isClosed_submodule`, `PatchingModule.map_apply`, `PatchingModule.mem_smul_top`
`PatchingModule` 📖	CompOp	28 math math: `instIsScalarTowerPatchingAlgebraPatchingModule`, `instFreePatchingModule`, `smul_lemma`, `instFinitePatchingModule`, `instT2SpacePatchingModule`, `instFinitePatchingAlgebraPatchingModule`, `PatchingAlgebra.faithfulSMul`, `PatchingModule.map_surjective`, `instTotallyDisconnectedSpacePatchingModule`, `PatchingModule.mapEquiv_apply`, `instIsScalarTowerForallPatchingModule`, `PatchingModule.mapEquiv_symm_apply`, `PatchingModule.mapOfIsPatchingSystem_bijective`, `instIsTopologicalAddGroupPatchingModule`, `smul_lemma₁`, `PatchingModule.continuous_ofPi`, `PatchingModule.map_id`, `PatchingModule.smul_apply`, `PatchingModule.incl_apply`, `PatchingModule.toConst_surjective`, `instContinuousSMulPatchingModule`, `smul_lemma₀`, `PatchingModule.rank_patchingModule`, `PatchingModule.map_comp_apply`, `PatchingModule.map_comp`, `PatchingModule.map_apply`, `PatchingModule.ker_map_mkQ`, `PatchingModule.mem_smul_top`
`instAddCommGroupPatchingModule` 📖	CompOp	25 math math: `instIsScalarTowerPatchingAlgebraPatchingModule`, `instFreePatchingModule`, `smul_lemma`, `instFinitePatchingModule`, `instFinitePatchingAlgebraPatchingModule`, `PatchingModule.map_surjective`, `PatchingModule.mapEquiv_apply`, `instIsScalarTowerForallPatchingModule`, `PatchingModule.mapEquiv_symm_apply`, `PatchingModule.mapOfIsPatchingSystem_bijective`, `instIsTopologicalAddGroupPatchingModule`, `smul_lemma₁`, `PatchingModule.continuous_ofPi`, `PatchingModule.map_id`, `PatchingModule.smul_apply`, `PatchingModule.incl_apply`, `PatchingModule.toConst_surjective`, `instContinuousSMulPatchingModule`, `smul_lemma₀`, `PatchingModule.rank_patchingModule`, `PatchingModule.map_comp_apply`, `PatchingModule.map_comp`, `PatchingModule.map_apply`, `PatchingModule.ker_map_mkQ`, `PatchingModule.mem_smul_top`
`instModuleForallPatchingModule` 📖	CompOp	11 math math: `PatchingModule.map_surjective`, `PatchingModule.mapEquiv_apply`, `instIsScalarTowerForallPatchingModule`, `PatchingModule.mapEquiv_symm_apply`, `PatchingModule.map_id`, `PatchingModule.incl_apply`, `smul_lemma₀`, `PatchingModule.map_comp_apply`, `PatchingModule.map_comp`, `PatchingModule.map_apply`, `PatchingModule.ker_map_mkQ`
`instModulePatchingModule` 📖	CompOp	14 math math: `instIsScalarTowerPatchingAlgebraPatchingModule`, `instFreePatchingModule`, `smul_lemma`, `instFinitePatchingModule`, `instIsScalarTowerForallPatchingModule`, `PatchingModule.mapOfIsPatchingSystem_bijective`, `smul_lemma₁`, `PatchingModule.continuous_ofPi`, `PatchingModule.smul_apply`, `PatchingModule.toConst_surjective`, `instContinuousSMulPatchingModule`, `PatchingModule.rank_patchingModule`, `PatchingModule.ker_map_mkQ`, `PatchingModule.mem_smul_top`
`instOrderTopOpenIdeals` 📖	CompOp	—
`instSemilatticeInfOpenIdeals` 📖	CompOp	1 math math: `PatchingAlgebra.smulData.f_mono`
`instTopologicalSpacePatchingModule` 📖	CompOp	5 math math: `instT2SpacePatchingModule`, `instTotallyDisconnectedSpacePatchingModule`, `instIsTopologicalAddGroupPatchingModule`, `PatchingModule.continuous_ofPi`, `instContinuousSMulPatchingModule`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instContinuousSMulComponentValIdealIsOpenCoe` 📖	mathematical	—	`PatchingModule.Component` `instAddCommGroupUltraProduct` `instModuleUltraProduct` `instTopologicalSpaceUltraProduct`	—	`instIsTopologicalAddGroupUltraProduct` `instDiscreteTopologyUltraProduct` `UltraProduct.πₗ_surjective` `instIsScalarTowerForallUltraProduct`
`instContinuousSMulPatchingModule` 📖	mathematical	—	`PatchingModule` `instAddCommGroupPatchingModule` `instModulePatchingModule` `instTopologicalSpacePatchingModule`	—	`instIsScalarTowerForallUltraProduct` `instContinuousSMulComponentValIdealIsOpenCoe`
`instFiniteComponentValIdealIsOpenCoeOfUniformlyBoundedRankOfFreeQuotientAnnihilator` 📖	mathematical	—	`PatchingModule.Component`	—	`instIsScalarTowerForallUltraProduct` `UltraProduct.exists_bijective_of_bddAbove_card` `Module.UniformlyBoundedRank.finite_quotient_smul` `Module.UniformlyBoundedRank.card_quotient_le`
`instFinitePatchingModule` 📖	mathematical	—	`PatchingModule` `instAddCommGroupPatchingModule` `instModulePatchingModule`	—	`PatchingModule.mapOfIsPatchingSystem_bijective`
`instFiniteQuotientIdealAnnihilator_fLT` 📖	—	—	—	—	`Module.UniformlyBoundedRank.rank_lt_bound`
`instFinite_fLT` 📖	—	—	—	—	`instFiniteQuotientIdealAnnihilator_fLT`
`instFreePatchingModule` 📖	mathematical	—	`PatchingModule` `instAddCommGroupPatchingModule` `instModulePatchingModule`	—	`PatchingModule.mapOfIsPatchingSystem_bijective`
`instIsScalarTowerForallPatchingModule` 📖	mathematical	—	`PatchingModule` `instAddCommGroupPatchingModule` `instModuleForallPatchingModule` `instModulePatchingModule`	—	`instIsScalarTowerForallUltraProduct`
`instIsTopologicalAddGroupPatchingModule` 📖	mathematical	—	`PatchingModule` `instTopologicalSpacePatchingModule` `instAddCommGroupPatchingModule`	—	`instIsTopologicalAddGroupUltraProduct`
`instT2SpacePatchingModule` 📖	mathematical	—	`PatchingModule` `instTopologicalSpacePatchingModule`	—	`instDiscreteTopologyUltraProduct`
`instTotallyDisconnectedSpacePatchingModule` 📖	mathematical	—	`PatchingModule` `instTopologicalSpacePatchingModule`	—	`instTotallyDisconnectedSpaceOfDiscreteTopology_fLT` `instDiscreteTopologyUltraProduct`

---

← Back to Index