Ultraproduct

📁 Source: FLT/Patching/Ultraproduct.lean

Statistics

Metric	Count
Definitions `UltraProduct`, `map`, `mapRingHom`, `π`, `πₗ`, `eventuallyProd`, `instAddCommGroupUltraProduct`, `instAlgebraForallUltraProduct`, `instAlgebraUltraProduct`, `instCommRingUltraProduct`, `instModuleForallUltraProduct`, `instModuleUltraProduct`, `instModuleUltraProduct_1`, `instSMulUltraProduct`, `instTopologicalSpaceUltraProduct`	15
Theorems `bijective_of_eventually_bijective`, `continuous_of_bddAbove_card`, `exists_algEquiv_of_bddAbove_card`, `exists_bijective_of_bddAbove_card`, `exists_ringEquiv_of_bddAbove_card`, `instIsScalarTower`, `isUnit_π_iff`, `mapRingHom_surjective`, `mapRingHom_π`, `map_surjective`, `map_πₗ`, `surjective_of_bddAbove_card`, `surjective_of_eventually_surjective`, `π_eq_iff`, `π_eq_zero_iff`, `π_smul`, `π_surjective`, `πₗ_eq_iff`, `πₗ_eq_zero`, `πₗ_surjective`, `isPrime`, `eventuallyProd_eq_sup`, `eventuallyProd_mono_left`, `eventuallyProd_mono_right`, `instDiscreteTopologyUltraProduct`, `instIsLocalHomUltraProductRingHomMapRingHom`, `instIsScalarTowerForallUltraProduct`, `instIsScalarTowerForallUltraProduct_1`, `instIsScalarTowerUltraProduct`, `instIsTopologicalAddGroupUltraProduct`, `instIsTopologicalRingUltraProduct`, `mem_eventuallyProd`	32
Total	47

UltraProduct

Definitions

Name	Category	Theorems
`map` 📖	CompOp	2 math math: `map_surjective`, `map_πₗ`
`mapRingHom` 📖	CompOp	3 math math: `instIsLocalHomUltraProductRingHomMapRingHom`, `mapRingHom_π`, `mapRingHom_surjective`
`π` 📖	CompOp	10 math math: `π_eq_zero_iff`, `surjective_of_bddAbove_card`, `PatchingAlgebra.ofPi_apply`, `mapRingHom_π`, `π_smul`, `π_surjective`, `isUnit_π_iff`, `π_eq_iff`, `exists_ringEquiv_of_bddAbove_card`, `continuous_of_bddAbove_card`
`πₗ` 📖	CompOp	9 math math: `exists_bijective_of_bddAbove_card`, `πₗ_surjective`, `πₗ_eq_iff`, `surjective_of_eventually_surjective`, `PatchingModule.ofPi_apply`, `bijective_of_eventually_bijective`, `PatchingModule.incl_apply`, `πₗ_eq_zero`, `map_πₗ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_of_eventually_bijective` 📖	mathematical	—	`UltraProduct` `instAddCommGroupUltraProduct` `instModuleUltraProduct` `instModuleForallUltraProduct` `instIsScalarTowerForallUltraProduct` `πₗ`	—	`instIsScalarTowerForallUltraProduct` `πₗ_surjective` `πₗ_eq_iff`
`continuous_of_bddAbove_card` 📖	mathematical	—	`UltraProduct` `instTopologicalSpaceUltraProduct` `instCommRingUltraProduct` `π`	—	`exists_ringEquiv_of_bddAbove_card` `instIsTopologicalRingUltraProduct` `instDiscreteTopologyUltraProduct`
`exists_algEquiv_of_bddAbove_card` 📖	mathematical	—	`UltraProduct` `instCommRingUltraProduct` `instAlgebraUltraProduct`	—	`TopologicalAlgebraTypeCardLT.isHomeomorph_equivOfAlgebra` `instFiniteTopologicalAlgebraTypeCardLT` `instIsScalarTowerForallUltraProduct` `bijective_of_eventually_bijective` `πₗ_eq_iff`
`exists_bijective_of_bddAbove_card` 📖	mathematical	—	`UltraProduct` `instAddCommGroupUltraProduct` `instModuleUltraProduct` `instModuleForallUltraProduct` `instIsScalarTowerForallUltraProduct` `πₗ`	—	`instIsScalarTowerForallUltraProduct` `instFiniteModuleTypeCardLT` `bijective_of_eventually_bijective`
`exists_ringEquiv_of_bddAbove_card` 📖	mathematical	—	`UltraProduct` `instCommRingUltraProduct` `π`	—	`exists_algEquiv_of_bddAbove_card`
`instIsScalarTower` 📖	mathematical	—	`UltraProduct` `instAddCommGroupUltraProduct` `instModuleUltraProduct`	—	—
`isUnit_π_iff` 📖	mathematical	—	`UltraProduct` `instCommRingUltraProduct` `π`	—	`π_surjective`
`mapRingHom_surjective` 📖	mathematical	—	`UltraProduct` `instCommRingUltraProduct` `mapRingHom`	—	`map_surjective`
`mapRingHom_π` 📖	mathematical	—	`UltraProduct` `instCommRingUltraProduct` `mapRingHom` `π`	—	—
`map_surjective` 📖	mathematical	—	`UltraProduct` `instAddCommGroupUltraProduct` `instModuleForallUltraProduct` `map`	—	`πₗ_surjective`
`map_πₗ` 📖	mathematical	—	`UltraProduct` `instAddCommGroupUltraProduct` `instModuleForallUltraProduct` `map` `πₗ`	—	—
`surjective_of_bddAbove_card` 📖	mathematical	—	`UltraProduct` `instCommRingUltraProduct` `π`	—	`exists_ringEquiv_of_bddAbove_card`
`surjective_of_eventually_surjective` 📖	mathematical	—	`UltraProduct` `instAddCommGroupUltraProduct` `instModuleUltraProduct` `instModuleForallUltraProduct` `instIsScalarTowerForallUltraProduct` `πₗ`	—	`instIsScalarTowerForallUltraProduct` `πₗ_surjective` `πₗ_eq_iff`
`π_eq_iff` 📖	mathematical	—	`UltraProduct` `instCommRingUltraProduct` `π`	—	—
`π_eq_zero_iff` 📖	mathematical	—	`UltraProduct` `instCommRingUltraProduct` `π`	—	`π_eq_iff`
`π_smul` 📖	mathematical	—	`UltraProduct` `instSMulUltraProduct` `instCommRingUltraProduct` `π` `instAddCommGroupUltraProduct` `instModuleForallUltraProduct`	—	—
`π_surjective` 📖	mathematical	—	`UltraProduct` `instCommRingUltraProduct` `π`	—	—
`πₗ_eq_iff` 📖	mathematical	—	`UltraProduct` `instAddCommGroupUltraProduct` `instModuleForallUltraProduct` `πₗ`	—	—
`πₗ_eq_zero` 📖	mathematical	—	`UltraProduct` `instAddCommGroupUltraProduct` `instModuleForallUltraProduct` `πₗ`	—	—
`πₗ_surjective` 📖	mathematical	—	`UltraProduct` `instAddCommGroupUltraProduct` `instModuleForallUltraProduct` `πₗ`	—	—

(root)

Definitions

Name	Category	Theorems
`UltraProduct` 📖	CompOp	30 math math: `UltraProduct.exists_bijective_of_bddAbove_card`, `instIsLocalHomUltraProductRingHomMapRingHom`, `UltraProduct.π_eq_zero_iff`, `UltraProduct.surjective_of_bddAbove_card`, `UltraProduct.πₗ_surjective`, `UltraProduct.instIsScalarTower`, `instIsTopologicalAddGroupUltraProduct`, `UltraProduct.πₗ_eq_iff`, `PatchingAlgebra.ofPi_apply`, `instIsScalarTowerForallUltraProduct_1`, `UltraProduct.surjective_of_eventually_surjective`, `instDiscreteTopologyUltraProduct`, `PatchingModule.ofPi_apply`, `UltraProduct.map_surjective`, `UltraProduct.mapRingHom_π`, `UltraProduct.π_smul`, `UltraProduct.bijective_of_eventually_bijective`, `instIsTopologicalRingUltraProduct`, `PatchingModule.incl_apply`, `UltraProduct.mapRingHom_surjective`, `instIsScalarTowerUltraProduct`, `instIsScalarTowerForallUltraProduct`, `UltraProduct.π_surjective`, `UltraProduct.isUnit_π_iff`, `UltraProduct.π_eq_iff`, `UltraProduct.exists_algEquiv_of_bddAbove_card`, `UltraProduct.exists_ringEquiv_of_bddAbove_card`, `UltraProduct.πₗ_eq_zero`, `UltraProduct.map_πₗ`, `UltraProduct.continuous_of_bddAbove_card`
`eventuallyProd` 📖	CompOp	9 math math: `eventuallyProd_vanishingFilter_le`, `eventuallyProd_mono_right`, `vanishingFilter_gc`, `eventuallyProd_eq_sup`, `eventuallyProd.isPrime`, `vanishingFilter_eventuallyProd`, `eventuallyProd_mono_left`, `vanishingFilter_le`, `mem_eventuallyProd`
`instAddCommGroupUltraProduct` 📖	CompOp	25 math math: `UltraProduct.exists_bijective_of_bddAbove_card`, `UltraProduct.πₗ_surjective`, `UltraProduct.instIsScalarTower`, `instIsTopologicalAddGroupUltraProduct`, `UltraProduct.πₗ_eq_iff`, `instIsScalarTowerForallUltraProduct_1`, `UltraProduct.surjective_of_eventually_surjective`, `PatchingModule.mapEquiv_apply`, `PatchingModule.ofPi_surjective`, `PatchingModule.componentMapModule_surjective`, `PatchingModule.ofPi_apply`, `UltraProduct.map_surjective`, `UltraProduct.π_smul`, `PatchingModule.smul_apply`, `UltraProduct.bijective_of_eventually_bijective`, `PatchingModule.incl_apply`, `PatchingModule.ker_componentMapModule_mkQ`, `instIsScalarTowerUltraProduct`, `instIsScalarTowerForallUltraProduct`, `instContinuousSMulComponentValIdealIsOpenCoe`, `PatchingModule.isClosed_submodule`, `PatchingModule.map_apply`, `UltraProduct.πₗ_eq_zero`, `UltraProduct.map_πₗ`, `PatchingModule.mem_smul_top`
`instAlgebraForallUltraProduct` 📖	CompOp	1 math math: `instIsScalarTowerForallUltraProduct_1`
`instAlgebraUltraProduct` 📖	CompOp	3 math math: `PatchingAlgebra.componentEquiv`, `instIsScalarTowerUltraProduct`, `UltraProduct.exists_algEquiv_of_bddAbove_card`
`instCommRingUltraProduct` 📖	CompOp	25 math math: `instIsLocalHomUltraProductRingHomMapRingHom`, `UltraProduct.π_eq_zero_iff`, `UltraProduct.surjective_of_bddAbove_card`, `instIsLocalHomSubtypeForallComponentMemSubringSubringRingHomCompEvalRingHomNatSubtypeOfNeZero`, `PatchingAlgebra.ofPi_surjective`, `PatchingAlgebra.ofPi_apply`, `PatchingAlgebra.componentEquiv`, `instIsScalarTowerForallUltraProduct_1`, `instIsLocalHomComponentRingHomComponentMapOfNeZeroNat`, `instIsLocalHomSubtypeForallComponentMemSubringSubringRingHomSubtype`, `UltraProduct.mapRingHom_π`, `UltraProduct.π_smul`, `instIsTopologicalRingUltraProduct`, `PatchingAlgebra.map_apply`, `PatchingAlgebra.isClosed_subring`, `UltraProduct.mapRingHom_surjective`, `instIsScalarTowerUltraProduct`, `PatchingAlgebra.componentMapRingHom_surjective`, `UltraProduct.π_surjective`, `UltraProduct.isUnit_π_iff`, `instIsLocalRingComponentOfNeZeroNat`, `UltraProduct.π_eq_iff`, `UltraProduct.exists_algEquiv_of_bddAbove_card`, `UltraProduct.exists_ringEquiv_of_bddAbove_card`, `UltraProduct.continuous_of_bddAbove_card`
`instModuleForallUltraProduct` 📖	CompOp	21 math math: `UltraProduct.exists_bijective_of_bddAbove_card`, `UltraProduct.πₗ_surjective`, `UltraProduct.πₗ_eq_iff`, `instIsScalarTowerForallUltraProduct_1`, `UltraProduct.surjective_of_eventually_surjective`, `PatchingModule.mapEquiv_apply`, `PatchingModule.ofPi_surjective`, `PatchingModule.componentMapModule_surjective`, `PatchingModule.ofPi_apply`, `UltraProduct.map_surjective`, `UltraProduct.π_smul`, `PatchingModule.smul_apply`, `UltraProduct.bijective_of_eventually_bijective`, `PatchingModule.incl_apply`, `PatchingModule.ker_componentMapModule_mkQ`, `instIsScalarTowerForallUltraProduct`, `PatchingModule.isClosed_submodule`, `PatchingModule.map_apply`, `UltraProduct.πₗ_eq_zero`, `UltraProduct.map_πₗ`, `PatchingModule.mem_smul_top`
`instModuleUltraProduct` 📖	CompOp	10 math math: `UltraProduct.exists_bijective_of_bddAbove_card`, `UltraProduct.instIsScalarTower`, `UltraProduct.surjective_of_eventually_surjective`, `PatchingModule.smul_apply`, `UltraProduct.bijective_of_eventually_bijective`, `PatchingModule.ker_componentMapModule_mkQ`, `instIsScalarTowerUltraProduct`, `instIsScalarTowerForallUltraProduct`, `instContinuousSMulComponentValIdealIsOpenCoe`, `PatchingModule.mem_smul_top`
`instModuleUltraProduct_1` 📖	CompOp	—
`instSMulUltraProduct` 📖	CompOp	3 math math: `instIsScalarTowerForallUltraProduct_1`, `UltraProduct.π_smul`, `instIsScalarTowerUltraProduct`
`instTopologicalSpaceUltraProduct` 📖	CompOp	8 math math: `instIsTopologicalAddGroupUltraProduct`, `instDiscreteTopologyUltraProduct`, `instIsTopologicalRingUltraProduct`, `PatchingAlgebra.isClosed_subring`, `instT2SpaceComponent`, `instContinuousSMulComponentValIdealIsOpenCoe`, `PatchingModule.isClosed_submodule`, `UltraProduct.continuous_of_bddAbove_card`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventuallyProd_eq_sup` 📖	mathematical	—	`eventuallyProd` `Submodule.pi'`	—	—
`eventuallyProd_mono_left` 📖	mathematical	—	`eventuallyProd`	—	—
`eventuallyProd_mono_right` 📖	mathematical	—	`eventuallyProd`	—	—
`instDiscreteTopologyUltraProduct` 📖	mathematical	—	`UltraProduct` `instTopologicalSpaceUltraProduct`	—	—
`instIsLocalHomUltraProductRingHomMapRingHom` 📖	mathematical	—	`UltraProduct` `instCommRingUltraProduct` `UltraProduct.mapRingHom`	—	`UltraProduct.π_surjective`
`instIsScalarTowerForallUltraProduct` 📖	mathematical	—	`UltraProduct` `instAddCommGroupUltraProduct` `instModuleForallUltraProduct` `instModuleUltraProduct`	—	`UltraProduct.πₗ_surjective`
`instIsScalarTowerForallUltraProduct_1` 📖	mathematical	—	`UltraProduct` `instCommRingUltraProduct` `instAlgebraForallUltraProduct` `instSMulUltraProduct` `instAddCommGroupUltraProduct` `instModuleForallUltraProduct`	—	`UltraProduct.π_surjective` `UltraProduct.π_smul`
`instIsScalarTowerUltraProduct` 📖	mathematical	—	`UltraProduct` `instCommRingUltraProduct` `instAlgebraUltraProduct` `instSMulUltraProduct` `instAddCommGroupUltraProduct` `instModuleUltraProduct`	—	`UltraProduct.π_surjective` `UltraProduct.π_smul` `instIsScalarTowerForallUltraProduct`
`instIsTopologicalAddGroupUltraProduct` 📖	mathematical	—	`UltraProduct` `instTopologicalSpaceUltraProduct` `instAddCommGroupUltraProduct`	—	`instDiscreteTopologyUltraProduct`
`instIsTopologicalRingUltraProduct` 📖	mathematical	—	`UltraProduct` `instTopologicalSpaceUltraProduct` `instCommRingUltraProduct`	—	`instDiscreteTopologyUltraProduct`
`mem_eventuallyProd` 📖	mathematical	—	`eventuallyProd`	—	—

eventuallyProd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPrime` 📖	mathematical	—	`eventuallyProd`	—	—

---

← Back to Index