Over

📁 Source: FLT/Patching/Over.lean

Statistics

Metric	Count
Definitions quotientTo, quotientToOver, quotientEquiv, quotientEquivOver, quotientTo, liftModIdeal, liftModIdealEquiv	7
Theorems surjective_quotientToOver, ker_componentMapModule_mkQ, ker_map_mkQ, mem_smul_top, instSubsingletonComponentTopIdeal	5
Total	12

PatchingAlgebra

Definitions

Name	Category	Theorems
quotientTo 📖	CompOp	—
quotientToOver 📖	CompOp	2 math math: smul_lemma, surjective_quotientToOver

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
surjective_quotientToOver 📖	mathematical	IsLocalRing.IsAdicTopology	PatchingAlgebra instCommRingPatchingAlgebra instAlgebraPatchingAlgebra quotientToOver	—	map_surjective

PatchingModule

Definitions

Name	Category	Theorems
quotientEquiv 📖	CompOp	—
quotientEquivOver 📖	CompOp	1 math math: smul_lemma
quotientTo 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ker_componentMapModule_mkQ 📖	mathematical	—	Component instAddCommGroupUltraProduct instModuleUltraProduct instModuleForallUltraProduct instIsScalarTowerForallUltraProduct componentMapModule	—	instIsScalarTowerForallUltraProduct Module.UniformlyBoundedRank.finite_quotient_smul UltraProduct.exists_bijective_of_bddAbove_card Module.UniformlyBoundedRank.card_quotient_le UltraProduct.bijective_of_eventually_bijective Submodule.comap_smul_of_surjective
ker_map_mkQ 📖	mathematical	—	PatchingModule instAddCommGroupPatchingModule instModulePatchingModule instModuleForallPatchingModule instIsScalarTowerForallPatchingModule map	—	instIsScalarTowerForallPatchingModule instIsScalarTowerForallUltraProduct ker_componentMapModule_mkQ mem_smul_top ofPi_surjective Submodule.comap_smul_of_surjective
mem_smul_top 📖	mathematical	—	PatchingModule instAddCommGroupPatchingModule instModulePatchingModule Component instAddCommGroupUltraProduct instModuleUltraProduct OpenIdeals instModuleForallUltraProduct submodule	—	instIsScalarTowerForallUltraProduct instFiniteComponentValIdealIsOpenCoeOfUniformlyBoundedRankOfFreeQuotientAnnihilator UltraProduct.πₗ_surjective nonempty_inverseLimit_of_finite

Submodule

Definitions

Name	Category	Theorems
liftModIdeal 📖	CompOp	—
liftModIdealEquiv 📖	CompOp	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSubsingletonComponentTopIdeal 📖	mathematical	—	PatchingModule.Component	—	—

---

← Back to Index