Documentation Verification Report

Algebra

📁 Source: FLT/Patching/Algebra.lean

Statistics

Metric	Count
Definitions `UniformlyBoundedRank`, `PatchingAlgebra`, `Component`, `componentMap`, `componentMapRingHom`, `constEquiv`, `incl`, `lift`, `map`, `mapEquiv`, `ofPi`, `subalgebra`, `subring`, `instAlgebraPatchingAlgebra`, `instCommRingPatchingAlgebra`, `instTopologicalSpacePatchingAlgebra`	16
Theorems `cond`, `algebraMap_continuous`, `algebraMap_surjective`, `componentEquiv`, `componentMapRingHom_surjective`, `continuous_lift`, `isClosed_subring`, `lift_surjective`, `mapEquiv_apply`, `mapEquiv_symm_apply`, `map_apply`, `map_comp`, `map_comp_apply`, `map_id`, `map_surjective`, `ofPi_apply`, `ofPi_surjective`, `continuous_of_finite_of_compact`, `instCompactSpacePatchingAlgebra`, `instFiniteComponent`, `instIsLocalHomComponentRingHomComponentMapOfNeZeroNat`, `instIsLocalHomSubtypeForallComponentMemSubringSubringRingHomCompEvalRingHomNatSubtypeOfNeZero`, `instIsLocalHomSubtypeForallComponentMemSubringSubringRingHomSubtype`, `instIsLocalRingComponentOfNeZeroNat`, `instIsLocalRingPatchingAlgebra`, `instIsTopologicalRingPatchingAlgebra`, `instNontrivialComponentOfNeZeroNat`, `instNontrivialForallComponent`, `instNontrivialPatchingAlgebra`, `instSubsingletonComponentOfNatNat`, `instT2SpaceComponent`, `instT2SpacePatchingAlgebra`, `instTotallyDisconnectedSpacePatchingAlgebra`	33
Total	49

Algebra

Definitions

Name	Category	Theorems
`UniformlyBoundedRank` 📖	CompData	—

Algebra.UniformlyBoundedRank

Theorems

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

PatchingAlgebra

Definitions

Name	Category	Theorems
`Component` 📖	CompOp	14 math math: `instIsLocalHomSubtypeForallComponentMemSubringSubringRingHomCompEvalRingHomNatSubtypeOfNeZero`, `ofPi_surjective`, `ofPi_apply`, `componentEquiv`, `instSubsingletonComponentOfNatNat`, `instIsLocalHomComponentRingHomComponentMapOfNeZeroNat`, `instIsLocalHomSubtypeForallComponentMemSubringSubringRingHomSubtype`, `map_apply`, `isClosed_subring`, `instFiniteComponent`, `componentMapRingHom_surjective`, `instT2SpaceComponent`, `instIsLocalRingComponentOfNeZeroNat`, `instNontrivialComponentOfNeZeroNat`
`componentMap` 📖	CompOp	1 math math: `instIsLocalHomComponentRingHomComponentMapOfNeZeroNat`
`componentMapRingHom` 📖	CompOp	2 math math: `map_apply`, `componentMapRingHom_surjective`
`constEquiv` 📖	CompOp	1 math math: `smul_lemma₁`
`incl` 📖	CompOp	—
`lift` 📖	CompOp	2 math math: `lift_surjective`, `continuous_lift`
`map` 📖	CompOp	8 math math: `map_id`, `mapEquiv_apply`, `map_apply`, `smul_lemma₀`, `map_comp`, `map_comp_apply`, `map_surjective`, `mapEquiv_symm_apply`
`mapEquiv` 📖	CompOp	2 math math: `mapEquiv_apply`, `mapEquiv_symm_apply`
`ofPi` 📖	CompOp	2 math math: `ofPi_surjective`, `ofPi_apply`
`subalgebra` 📖	CompOp	—
`subring` 📖	CompOp	4 math math: `instIsLocalHomSubtypeForallComponentMemSubringSubringRingHomCompEvalRingHomNatSubtypeOfNeZero`, `instIsLocalHomSubtypeForallComponentMemSubringSubringRingHomSubtype`, `map_apply`, `isClosed_subring`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_continuous` 📖	mathematical	—	`PatchingAlgebra` `instTopologicalSpacePatchingAlgebra` `instCommRingPatchingAlgebra` `instAlgebraPatchingAlgebra`	—	`instFiniteComponent` `RingHom.continuous_of_finite_of_compact` `IsLocalRing.instT2SpaceOfIsNoetherianRing_fLT` `instIsTopologicalRingUltraProduct`
`algebraMap_surjective` 📖	mathematical	—	`PatchingAlgebra` `instCommRingPatchingAlgebra` `instAlgebraPatchingAlgebra`	—	`denseRange_inverseLimit` `instDiscreteTopologyUltraProduct` `IsLocalRing.instT2SpaceOfIsNoetherianRing_fLT` `instIsScalarTowerForallUltraProduct` `UltraProduct.surjective_of_eventually_surjective` `instT2SpacePatchingAlgebra` `algebraMap_continuous`
`componentEquiv` 📖	mathematical	`IsLocalRing.IsAdicTopology`	`Component` `instCommRingUltraProduct` `instAlgebraUltraProduct`	—	`Algebra.UniformlyBoundedRank.cond` `UltraProduct.exists_algEquiv_of_bddAbove_card` `IsLocalRing.instDiscreteTopologyQuotientIdealHPowNatMaximalIdeal_fLT` `IsLocalRing.isOpen_maximalIdeal_pow''` `IsLocalRing.instNonarchimedeanRing_fLT`
`componentMapRingHom_surjective` 📖	mathematical	—	`Component` `instCommRingUltraProduct` `componentMapRingHom`	—	`UltraProduct.mapRingHom_surjective`
`continuous_lift` 📖	mathematical	`IsLocalRing.IsAdicTopology`	`PatchingAlgebra` `instTopologicalSpacePatchingAlgebra` `instCommRingPatchingAlgebra` `lift`	—	`Algebra.UniformlyBoundedRank.cond` `UltraProduct.continuous_of_bddAbove_card` `IsLocalRing.instDiscreteTopologyQuotientIdealHPowNatMaximalIdeal_fLT` `IsLocalRing.isOpen_maximalIdeal_pow''` `IsLocalRing.instNonarchimedeanRing_fLT`
`isClosed_subring` 📖	mathematical	—	`Component` `instTopologicalSpaceUltraProduct` `instCommRingUltraProduct` `subring`	—	`instT2SpaceComponent`
`lift_surjective` 📖	mathematical	`IsLocalRing.IsAdicTopology`	`PatchingAlgebra` `instCommRingPatchingAlgebra` `lift`	—	`denseRange_inverseLimit` `instDiscreteTopologyUltraProduct` `Algebra.UniformlyBoundedRank.cond` `UltraProduct.surjective_of_bddAbove_card` `IsLocalRing.instDiscreteTopologyQuotientIdealHPowNatMaximalIdeal_fLT` `IsLocalRing.isOpen_maximalIdeal_pow''` `IsLocalRing.instNonarchimedeanRing_fLT` `instT2SpacePatchingAlgebra` `continuous_lift`
`mapEquiv_apply` 📖	mathematical	—	`PatchingAlgebra` `instCommRingPatchingAlgebra` `mapEquiv` `map`	—	—
`mapEquiv_symm_apply` 📖	mathematical	—	`PatchingAlgebra` `instCommRingPatchingAlgebra` `mapEquiv` `map`	—	—
`map_apply` 📖	mathematical	—	`Component` `instCommRingUltraProduct` `subring` `PatchingAlgebra` `instCommRingPatchingAlgebra` `map` `componentMapRingHom`	—	—
`map_comp` 📖	mathematical	—	`map` `PatchingAlgebra` `instCommRingPatchingAlgebra`	—	`map_comp_apply`
`map_comp_apply` 📖	mathematical	—	`PatchingAlgebra` `instCommRingPatchingAlgebra` `map`	—	`ofPi_surjective`
`map_id` 📖	mathematical	—	`map` `PatchingAlgebra` `instCommRingPatchingAlgebra`	—	`ofPi_surjective`
`map_surjective` 📖	mathematical	`IsLocalRing.IsAdicTopology`	`PatchingAlgebra` `instCommRingPatchingAlgebra` `map`	—	`UltraProduct.π_surjective` `componentMapRingHom_surjective` `nonempty_inverseLimit_of_finite` `instFiniteComponent`
`ofPi_apply` 📖	mathematical	—	`Component` `instCommRingUltraProduct` `ofPi` `UltraProduct` `UltraProduct.π`	—	—
`ofPi_surjective` 📖	mathematical	—	`Component` `instCommRingUltraProduct` `ofPi`	—	—

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_of_finite_of_compact` 📖	—	—	—	—	`IsLocalRing.isCompact_of_isNoetherianRing`

(root)

Definitions

Name	Category	Theorems
`PatchingAlgebra` 📖	CompOp	24 math math: `instIsScalarTowerPatchingAlgebraPatchingModule`, `smul_lemma`, `PatchingAlgebra.map_id`, `PatchingAlgebra.algebraMap_continuous`, `instFinitePatchingAlgebraPatchingModule`, `PatchingAlgebra.faithfulSMul`, `PatchingAlgebra.algebraMap_surjective`, `instIsTopologicalRingPatchingAlgebra`, `PatchingAlgebra.surjective_quotientToOver`, `smul_lemma₁`, `instT2SpacePatchingAlgebra`, `instCompactSpacePatchingAlgebra`, `PatchingAlgebra.mapEquiv_apply`, `PatchingAlgebra.map_apply`, `smul_lemma₀`, `PatchingAlgebra.map_comp`, `PatchingAlgebra.lift_surjective`, `instIsLocalRingPatchingAlgebra`, `PatchingAlgebra.map_comp_apply`, `instNontrivialPatchingAlgebra`, `PatchingAlgebra.map_surjective`, `PatchingAlgebra.mapEquiv_symm_apply`, `PatchingAlgebra.continuous_lift`, `instTotallyDisconnectedSpacePatchingAlgebra`
`instAlgebraPatchingAlgebra` 📖	CompOp	6 math math: `instIsScalarTowerPatchingAlgebraPatchingModule`, `smul_lemma`, `PatchingAlgebra.algebraMap_continuous`, `PatchingAlgebra.algebraMap_surjective`, `PatchingAlgebra.surjective_quotientToOver`, `smul_lemma₁`
`instCommRingPatchingAlgebra` 📖	CompOp	19 math math: `instIsScalarTowerPatchingAlgebraPatchingModule`, `smul_lemma`, `PatchingAlgebra.map_id`, `PatchingAlgebra.algebraMap_continuous`, `instFinitePatchingAlgebraPatchingModule`, `PatchingAlgebra.algebraMap_surjective`, `instIsTopologicalRingPatchingAlgebra`, `PatchingAlgebra.surjective_quotientToOver`, `smul_lemma₁`, `PatchingAlgebra.mapEquiv_apply`, `PatchingAlgebra.map_apply`, `smul_lemma₀`, `PatchingAlgebra.map_comp`, `PatchingAlgebra.lift_surjective`, `instIsLocalRingPatchingAlgebra`, `PatchingAlgebra.map_comp_apply`, `PatchingAlgebra.map_surjective`, `PatchingAlgebra.mapEquiv_symm_apply`, `PatchingAlgebra.continuous_lift`
`instTopologicalSpacePatchingAlgebra` 📖	CompOp	6 math math: `PatchingAlgebra.algebraMap_continuous`, `instIsTopologicalRingPatchingAlgebra`, `instT2SpacePatchingAlgebra`, `instCompactSpacePatchingAlgebra`, `PatchingAlgebra.continuous_lift`, `instTotallyDisconnectedSpacePatchingAlgebra`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompactSpacePatchingAlgebra` 📖	mathematical	`IsLocalRing.IsAdicTopology`	`PatchingAlgebra` `instTopologicalSpacePatchingAlgebra`	—	`instFiniteComponent` `PatchingAlgebra.isClosed_subring`
`instFiniteComponent` 📖	mathematical	`IsLocalRing.IsAdicTopology`	`PatchingAlgebra.Component`	—	`PatchingAlgebra.componentEquiv` `IsLocalRing.instNonarchimedeanRing_fLT` `instTopologicallyFGOfFiniteType` `IsLocalRing.isOpen_maximalIdeal_pow''`
`instIsLocalHomComponentRingHomComponentMapOfNeZeroNat` 📖	mathematical	—	`PatchingAlgebra.Component` `instCommRingUltraProduct` `PatchingAlgebra.componentMap`	—	`instIsLocalHomUltraProductRingHomMapRingHom`
`instIsLocalHomSubtypeForallComponentMemSubringSubringRingHomCompEvalRingHomNatSubtypeOfNeZero` 📖	mathematical	—	`PatchingAlgebra.Component` `instCommRingUltraProduct` `PatchingAlgebra.subring`	—	`instIsLocalHomSubtypeForallComponentMemSubringSubringRingHomSubtype` `IsUnit.pi_iff` `instIsLocalHomComponentRingHomComponentMapOfNeZeroNat`
`instIsLocalHomSubtypeForallComponentMemSubringSubringRingHomSubtype` 📖	mathematical	—	`PatchingAlgebra.Component` `instCommRingUltraProduct` `PatchingAlgebra.subring`	—	`IsUnit.pi_iff`
`instIsLocalRingComponentOfNeZeroNat` 📖	mathematical	`IsLocalRing.IsAdicTopology`	`PatchingAlgebra.Component` `instCommRingUltraProduct`	—	`PatchingAlgebra.componentEquiv` `IsLocalRing.instNonarchimedeanRing_fLT` `instTopologicallyFGOfFiniteType` `instNontrivialComponentOfNeZeroNat`
`instIsLocalRingPatchingAlgebra` 📖	mathematical	`IsLocalRing.IsAdicTopology`	`PatchingAlgebra` `instCommRingPatchingAlgebra`	—	`instNontrivialPatchingAlgebra` `instIsLocalHomSubtypeForallComponentMemSubringSubringRingHomSubtype` `IsUnit.pi_iff` `instIsLocalRingComponentOfNeZeroNat`
`instIsTopologicalRingPatchingAlgebra` 📖	mathematical	—	`PatchingAlgebra` `instTopologicalSpacePatchingAlgebra` `instCommRingPatchingAlgebra`	—	`instIsTopologicalRingUltraProduct`
`instNontrivialComponentOfNeZeroNat` 📖	mathematical	`IsLocalRing.IsAdicTopology`	`PatchingAlgebra.Component`	—	`PatchingAlgebra.componentEquiv` `IsLocalRing.instNonarchimedeanRing_fLT` `instTopologicallyFGOfFiniteType`
`instNontrivialForallComponent` 📖	—	`IsLocalRing.IsAdicTopology`	—	—	`instNontrivialComponentOfNeZeroNat`
`instNontrivialPatchingAlgebra` 📖	mathematical	`IsLocalRing.IsAdicTopology`	`PatchingAlgebra`	—	`instNontrivialForallComponent`
`instSubsingletonComponentOfNatNat` 📖	mathematical	`IsLocalRing.IsAdicTopology`	`PatchingAlgebra.Component`	—	`PatchingAlgebra.componentEquiv` `IsLocalRing.instNonarchimedeanRing_fLT` `instTopologicallyFGOfFiniteType`
`instT2SpaceComponent` 📖	mathematical	—	`PatchingAlgebra.Component` `instTopologicalSpaceUltraProduct`	—	`instDiscreteTopologyUltraProduct`
`instT2SpacePatchingAlgebra` 📖	mathematical	—	`PatchingAlgebra` `instTopologicalSpacePatchingAlgebra`	—	`instT2SpaceComponent`
`instTotallyDisconnectedSpacePatchingAlgebra` 📖	mathematical	—	`PatchingAlgebra` `instTopologicalSpacePatchingAlgebra`	—	`instTotallyDisconnectedSpaceOfDiscreteTopology_fLT` `instDiscreteTopologyUltraProduct`

---

← Back to Index