Documentation Verification Report

System

📁 Source: FLT/Patching/System.lean

Statistics

Metric	Count
Definitions `isModuleQuotient`, `isModuleQuotient'`, `smulData`, `f`, `instModuleComponentFComponentValIdealIsOpenCoe`, `instModulePatchingAlgebraPatchingModuleOfSmulData`, `instSMulIdealSubmoduleOfSMulCommClass_fLT`, `instSMulPatchingAlgebraPatchingModuleOfSmulData`, `instSmulData`, `instSmulData_1`	10
Theorems `faithfulSMul`, `f_mono`, `pow_f_smul_le`, `map_algebraMap_smul`, `eventually_eventually_eq_of_finite`, `instFinitePatchingAlgebraPatchingModule`, `instIsScalarTowerPatchingAlgebraPatchingModule`, `maximalIdeal_pow_bound_le_smul_top`, `smul_lemma`, `smul_lemma₀`, `smul_lemma₁`, `support_eq_top`	12
Total	22

IsPatchingSystem

Definitions

Name	Category	Theorems
`isModuleQuotient` 📖	CompOp	—
`isModuleQuotient'` 📖	CompOp	—

PatchingAlgebra

Definitions

Name	Category	Theorems
`smulData` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`faithfulSMul` 📖	mathematical	`IsLocalRing.IsAdicTopology` `Module.depth`	`PatchingAlgebra` `PatchingModule` `instSMulPatchingAlgebraPatchingModuleOfSmulData` `instSmulData`	—	`lift_surjective` `UltraProduct.π_eq_iff` `Module.UniformlyBoundedRank.rank_spec` `PatchingModule.rank_patchingModule` `instIsScalarTowerPatchingAlgebraPatchingModule` `instFinitePatchingModule` `Module.faithfulSMul_of_depth_eq_ringKrullDim` `Module.depth_le_dim` `Module.depth_le_of_free` `instFreePatchingModule` `Module.depth_of_isScalarTower`

PatchingAlgebra.smulData

Definitions

Name	Category	Theorems
`f` 📖	CompOp	2 math math: `f_mono`, `pow_f_smul_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`f_mono` 📖	mathematical	—	`OpenIdeals` `instSemilatticeInfOpenIdeals` `f`	—	—
`pow_f_smul_le` 📖	mathematical	—	`instSMulIdealSubmoduleOfSMulCommClass_fLT` `f`	—	—

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_algebraMap_smul` 📖	mathematical	—	`instSMulIdealSubmoduleOfSMulCommClass_fLT`	—	—

Ultrafilter

Theorems

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

(root)

Definitions

Name	Category	Theorems
`instModuleComponentFComponentValIdealIsOpenCoe` 📖	CompOp	—
`instModulePatchingAlgebraPatchingModuleOfSmulData` 📖	CompOp	2 math math: `smul_lemma`, `instFinitePatchingAlgebraPatchingModule`
`instSMulIdealSubmoduleOfSMulCommClass_fLT` 📖	CompOp	3 math math: `Submodule.map_algebraMap_smul`, `PatchingAlgebra.smulData.pow_f_smul_le`, `maximalIdeal_pow_bound_le_smul_top`
`instSMulPatchingAlgebraPatchingModuleOfSmulData` 📖	CompOp	4 math math: `instIsScalarTowerPatchingAlgebraPatchingModule`, `PatchingAlgebra.faithfulSMul`, `smul_lemma₁`, `smul_lemma₀`
`instSmulData` 📖	CompOp	3 math math: `smul_lemma`, `PatchingAlgebra.faithfulSMul`, `smul_lemma₀`
`instSmulData_1` 📖	CompOp	2 math math: `smul_lemma₁`, `smul_lemma₀`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFinitePatchingAlgebraPatchingModule` 📖	mathematical	—	`PatchingAlgebra` `PatchingModule` `instCommRingPatchingAlgebra` `instAddCommGroupPatchingModule` `instModulePatchingAlgebraPatchingModuleOfSmulData`	—	`instIsScalarTowerPatchingAlgebraPatchingModule` `instFinitePatchingModule`
`instIsScalarTowerPatchingAlgebraPatchingModule` 📖	mathematical	—	`PatchingAlgebra` `PatchingModule` `instCommRingPatchingAlgebra` `instAlgebraPatchingAlgebra` `instSMulPatchingAlgebraPatchingModuleOfSmulData` `instAddCommGroupPatchingModule` `instModulePatchingModule`	—	`UltraProduct.πₗ_surjective` `UltraProduct.πₗ_eq_iff`
`maximalIdeal_pow_bound_le_smul_top` 📖	mathematical	—	`instSMulIdealSubmoduleOfSMulCommClass_fLT` `Module.UniformlyBoundedRank.bound`	—	`Submodule.map_algebraMap_smul` `Module.UniformlyBoundedRank.finite_quotient_smul` `Module.UniformlyBoundedRank.card_quotient_le` `IsLocalRing.maximalIdeal_pow_card_smul_top_le`
`smul_lemma` 📖	mathematical	`instSMulIdealSubmoduleOfSMulCommClass_fLT`	`PatchingModule` `instAddCommGroupPatchingModule` `instModulePatchingModule` `PatchingModule.quotientEquivOver` `PatchingAlgebra` `instCommRingPatchingAlgebra` `instModulePatchingAlgebraPatchingModuleOfSmulData` `instSmulData` `instAlgebraPatchingAlgebra` `instIsScalarTowerPatchingAlgebraPatchingModule` `PatchingAlgebra.quotientToOver`	—	`instIsScalarTowerPatchingAlgebraPatchingModule` `instIsLocalHomRingHomToRingHom_fLT_1` `PatchingModule.ofPi_surjective` `PatchingAlgebra.ofPi_surjective` `smul_lemma₁` `smul_lemma₀`
`smul_lemma₀` 📖	mathematical	`instSMulIdealSubmoduleOfSMulCommClass_fLT`	`PatchingModule` `instAddCommGroupPatchingModule` `instModuleForallPatchingModule` `PatchingModule.map` `PatchingAlgebra` `instSMulPatchingAlgebraPatchingModuleOfSmulData` `instSmulData` `instSmulData_1` `instCommRingPatchingAlgebra` `PatchingAlgebra.map` `instIsLocalHomRingHomToRingHom_fLT_1`	—	`instIsLocalHomRingHomToRingHom_fLT_1` `PatchingModule.ofPi_surjective` `PatchingAlgebra.ofPi_surjective` `UltraProduct.πₗ_eq_iff` `PatchingAlgebra.smulData.pow_f_smul_le` `IsLocalRing.map_maximalIdeal` `Submodule.map_algebraMap_smul`
`smul_lemma₁` 📖	mathematical	—	`PatchingModule` `instAddCommGroupPatchingModule` `instModulePatchingModule` `PatchingModule.constEquiv` `PatchingAlgebra` `instSMulPatchingAlgebraPatchingModuleOfSmulData` `instSmulData_1` `instCommRingPatchingAlgebra` `instAlgebraPatchingAlgebra` `PatchingAlgebra.constEquiv`	—	—
`support_eq_top` 📖	—	`IsLocalRing.IsAdicTopology` `instSMulIdealSubmoduleOfSMulCommClass_fLT` `Module.depth`	—	—	`instFinite_fLT` `PatchingAlgebra.faithfulSMul` `PatchingAlgebra.surjective_quotientToOver` `instIsScalarTowerPatchingAlgebraPatchingModule` `smul_lemma` `instFinitePatchingAlgebraPatchingModule` `Submodule.map_algebraMap_smul`

---

← Back to Index