BaseChange

📁 Source: FLT/DedekindDomain/Completion/BaseChange.lean

Statistics

Metric	Count
Definitions `adicCompletionComapAlgEquiv`, `adicCompletionComapContinuousAlgEquiv`, `adicCompletionComapIntegerLinearEquiv`, `adicCompletionComapIntegerLinearMap`, `adicCompletionComapIntegerRingHom`, `adicCompletionComapRightContinuousAlgEquiv`, `adicCompletionComapSemialgHom`, `adicCompletionComapSemialgHom'`, `adicCompletionIntegersSubalgebra`, `adicCompletionTensorIntegerCoe`, `adicCompletion_RkOne`, `comap_algebra`, `comap_integer_algebra`, `comap_integer_algebra'`, `comap_pi_algebra`, `integerSubmodule`, `tensorAdicCompletionComapAlgHom`, `tensorAdicCompletionComapLinearMap`, `tensorAdicCompletionIntegersTo`, `tensorAdicCompletionIntegersToLinearMap`	20
Theorems `ofAdd_neg_ofNat_pow`, `inertiaDeg_eq_inertiaDeg`, `ramificationIdx_eq_ramificationIdx`, `adicCompletionComapAlgEquiv_integral`, `adicCompletionComapAlgHom_map_closure_is_closed`, `adicCompletionComapIntegerLinearEquiv_bijOn`, `adicCompletionComapIntegerLinearEquiv_tmul_apply`, `adicCompletionComapIntegerLinearMap_range_eq_integers`, `mapadicCompletionIntegers`, `adicCompletionComapSemialgHom_continuous`, `adicCompletionComap_coe`, `adicCompletionComap_isModuleTopology`, `adicCompletionTensorIntegerCoe_tmul`, `continuous_algebraMap`, `comap_algebra_continuousSmul`, `comap_algebra_finite`, `comap_integer_algebraMap`, `comap_integer_algebra_finite`, `comap_pi_algebra_finite`, `finrank_tensorProduct_adicCompletion_eq_finrank_pi_adicCompletion`, `instIsScalarTowerSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_fLT`, `instMulActionHomClassAlgHomTensorProductAdicCompletionForallValEqComap`, `instOneHomClassAlgHomTensorProductAdicCompletionForallValEqComap`, `prodAdicCompletionComap_isModuleTopology`, `prodAdicCompletionsIntegers_eq_closureIntegers`, `ramification_mul_inertia_eq_finrank_completion`, `tensorAdicCompletionComapAlgHom_bijective`, `tensorAdicCompletionComapAlgHom_tmul_apply`, `tensorAdicCompletionComapLinearMap_isOpenQuotientMap`, `tensorAdicCompletionComapLinearMap_surjective`, `tensorAdicCompletionIntegersToRange_eq_closureIntegers`, `tensorAdicCompletionIntegersToRange_subset_closureIntegers`, `tensorAdicCompletionIntegersTo_tmul`, `tensorAdicCompletionIsClopenRange`, `valued_adicCompletionComap`	35
Total	55

IsDedekindDomain.HeightOneSpectrum

Definitions

Name	Category	Theorems
`adicCompletionComapAlgEquiv` 📖	CompOp	—
`adicCompletionComapContinuousAlgEquiv` 📖	CompOp	—
`adicCompletionComapIntegerLinearEquiv` 📖	CompOp	3 math math: `adicCompletionComapIntegerLinearEquiv_bijOn`, `adicCompletionComapIntegerLinearEquiv_tmul_apply`, `IsDedekindDomain.FiniteAdeleRing.restrictedProduct_tensorProduct_equiv_restrictedProduct_prod_apply`
`adicCompletionComapIntegerLinearMap` 📖	CompOp	1 math math: `adicCompletionComapIntegerLinearMap_range_eq_integers`
`adicCompletionComapIntegerRingHom` 📖	CompOp	—
`adicCompletionComapRightContinuousAlgEquiv` 📖	CompOp	—
`adicCompletionComapSemialgHom` 📖	CompOp	6 math math: `IsDedekindDomain.cofinite_mapsTo_adicCompletionComapSemialgHom`, `adicCompletionComapSemialgHom.mapadicCompletionIntegers`, `valued_adicCompletionComap`, `comap_integer_algebraMap`, `adicCompletionComapSemialgHom_continuous`, `adicCompletionComap_coe`
`adicCompletionComapSemialgHom'` 📖	CompOp	—
`adicCompletionIntegersSubalgebra` 📖	CompOp	2 math math: `adicCompletionComapAlgEquiv_integral`, `prodAdicCompletionsIntegers_eq_closureIntegers`
`adicCompletionTensorIntegerCoe` 📖	CompOp	3 math math: `adicCompletionComapIntegerLinearEquiv_bijOn`, `IsDedekindDomain.range_adicCompletionTensorIntegerCoe_eq_lTensorRestriction`, `adicCompletionTensorIntegerCoe_tmul`
`adicCompletion_RkOne` 📖	CompOp	12 math math: `adicCompletionComapIntegerLinearMap_range_eq_integers`, `tensorAdicCompletionIsClopenRange`, `comap_pi_algebra_finite`, `adicCompletionComapAlgEquiv_integral`, `tensorAdicCompletionIntegersTo_tmul`, `tensorAdicCompletionIntegersToRange_eq_closureIntegers`, `tensorAdicCompletionIntegersToRange_subset_closureIntegers`, `comap_integer_algebra_finite`, `instMulActionHomClassAlgHomTensorProductAdicCompletionForallValEqComap`, `comap_algebra_finite`, `instOneHomClassAlgHomTensorProductAdicCompletionForallValEqComap`, `adicCompletionComapAlgHom_map_closure_is_closed`
`comap_algebra` 📖	CompOp	9 math math: `adicCompletionComap_isModuleTopology`, `adicCompletionComapIntegerLinearMap_range_eq_integers`, `adicCompletionComapIntegerLinearEquiv_tmul_apply`, `comap_algebra_continuousSmul`, `IsDedekindDomain.FiniteAdeleRing.mapSemialgHom_apply`, `ramification_mul_inertia_eq_finrank_completion`, `comap_algebra_finite`, `IsDedekindDomain.BaseChange.algebraMap_apply`, `tensorAdicCompletionComapAlgHom_tmul_apply`
`comap_integer_algebra` 📖	CompOp	4 math math: `adicCompletion.ramificationIdx_eq_ramificationIdx`, `adicCompletion.inertiaDeg_eq_inertiaDeg`, `comap_integer_algebraMap`, `comap_integer_algebra_finite`
`comap_integer_algebra'` 📖	CompOp	—
`comap_pi_algebra` 📖	CompOp	5 math math: `finrank_tensorProduct_adicCompletion_eq_finrank_pi_adicCompletion`, `tensorAdicCompletionComapLinearMap_isOpenQuotientMap`, `comap_pi_algebra_finite`, `prodAdicCompletionComap_isModuleTopology`, `tensorAdicCompletionComapLinearMap_surjective`
`integerSubmodule` 📖	CompOp	5 math math: `adicCompletionComapIntegerLinearEquiv_bijOn`, `IsDedekindDomain.range_adicCompletionTensorIntegerCoe_eq_lTensorRestriction`, `IsDedekindDomain.FiniteAdeleRing.restrictedProduct_prod_equiv_apply`, `IsDedekindDomain.FiniteAdeleRing.tensorEquivRestrictedProduct_tmul`, `IsDedekindDomain.FiniteAdeleRing.restrictedProduct_tensorProduct_equiv_restrictedProduct_prod_apply`
`tensorAdicCompletionComapAlgHom` 📖	CompOp	4 math math: `tensorAdicCompletionComapAlgHom_bijective`, `adicCompletionComapAlgEquiv_integral`, `adicCompletionComapAlgHom_map_closure_is_closed`, `tensorAdicCompletionComapAlgHom_tmul_apply`
`tensorAdicCompletionComapLinearMap` 📖	CompOp	2 math math: `tensorAdicCompletionComapLinearMap_isOpenQuotientMap`, `tensorAdicCompletionComapLinearMap_surjective`
`tensorAdicCompletionIntegersTo` 📖	CompOp	5 math math: `tensorAdicCompletionIsClopenRange`, `adicCompletionComapAlgEquiv_integral`, `tensorAdicCompletionIntegersTo_tmul`, `tensorAdicCompletionIntegersToRange_eq_closureIntegers`, `tensorAdicCompletionIntegersToRange_subset_closureIntegers`
`tensorAdicCompletionIntegersToLinearMap` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adicCompletionComapAlgEquiv_integral` 📖	mathematical	—	`adicCompletion_RkOne` `Extension` `comap` `instAlgebraWithVal_fLT_1` `instIsScalarTowerWithVal_fLT_1` `tensorAdicCompletionComapAlgHom` `tensorAdicCompletionIntegersTo` `adicCompletionIntegersSubalgebra`	—	`tensorAdicCompletionIntegersToRange_eq_closureIntegers` `prodAdicCompletionsIntegers_eq_closureIntegers` `instMulActionHomClassAlgHomTensorProductAdicCompletionForallValEqComap` `instOneHomClassAlgHomTensorProductAdicCompletionForallValEqComap` `adicCompletionComapAlgHom_map_closure_is_closed` `instIsScalarTowerWithVal_fLT_1` `tensorAdicCompletionComapLinearMap_isOpenQuotientMap`
`adicCompletionComapAlgHom_map_closure_is_closed` 📖	mathematical	—	`Extension` `comap` `instAlgebraWithVal_fLT_1` `tensorAdicCompletionComapAlgHom` `TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT` `adicCompletion_RkOne`	—	`tensorAdicCompletionComapLinearMap_isOpenQuotientMap` `tensorAdicCompletionIsClopenRange` `tensorAdicCompletionIntegersToRange_eq_closureIntegers`
`adicCompletionComapIntegerLinearEquiv_bijOn` 📖	mathematical	—	`instAlgebraWithVal_fLT_1` `Extension` `comap` `adicCompletionComapIntegerLinearEquiv` `adicCompletionTensorIntegerCoe` `integerSubmodule`	—	`instIsScalarTowerWithVal_fLT_1` `adicCompletionComapAlgEquiv_integral` `adicCompletionComapIntegerLinearEquiv_tmul_apply` `tensorAdicCompletionIntegersTo_tmul` `tensorAdicCompletionComapAlgHom_tmul_apply`
`adicCompletionComapIntegerLinearEquiv_tmul_apply` 📖	mathematical	—	`instAlgebraWithVal_fLT_1` `Extension` `comap` `adicCompletionComapIntegerLinearEquiv` `comap_algebra`	—	`adicCompletionComapIntegerLinearEquiv.eq_1` `IsDedekindDomain.linearEquivTensorProductModule_symm_tmul`
`adicCompletionComapIntegerLinearMap_range_eq_integers` 📖	mathematical	`comap`	`adicCompletion_RkOne` `TensorProduct.RightActions.instModule_fLT` `comap_algebra` `adicCompletionComapIntegerLinearMap`	—	`instIsScalarTowerWithVal_fLT_1` `adicCompletionComapAlgEquiv_integral`
`adicCompletionComapSemialgHom_continuous` 📖	mathematical	`comap`	`SemialgHom` `instAlgebraWithVal_fLT` `instFunLike` `adicCompletionComapSemialgHom`	—	—
`adicCompletionComap_coe` 📖	mathematical	`comap`	`SemialgHom` `instAlgebraWithVal_fLT` `instFunLike` `adicCompletionComapSemialgHom`	—	`SemialgHom.commutes`
`adicCompletionComap_isModuleTopology` 📖	mathematical	`comap`	`comap_algebra`	—	`comap_algebra_continuousSmul` `comap_algebra_finite`
`adicCompletionTensorIntegerCoe_tmul` 📖	mathematical	—	`instAlgebraWithVal_fLT_1` `adicCompletionTensorIntegerCoe`	—	—
`comap_algebra_continuousSmul` 📖	mathematical	`comap`	`comap_algebra`	—	`adicCompletionComapSemialgHom_continuous`
`comap_algebra_finite` 📖	mathematical	`comap`	`adicCompletion_RkOne` `comap_algebra`	—	`comap_pi_algebra_finite`
`comap_integer_algebraMap` 📖	mathematical	`comap`	`comap_integer_algebra` `SemialgHom` `instAlgebraWithVal_fLT` `instFunLike` `adicCompletionComapSemialgHom`	—	—
`comap_integer_algebra_finite` 📖	mathematical	`comap`	`adicCompletion_RkOne` `comap_integer_algebra`	—	`adicCompletionComapIntegerLinearMap_range_eq_integers` `TensorProduct.RightActions.instFinite_fLT`
`comap_pi_algebra_finite` 📖	mathematical	—	`Extension` `comap` `adicCompletion_RkOne` `comap_pi_algebra`	—	`TensorProduct.RightActions.instFinite_fLT` `tensorAdicCompletionComapLinearMap_surjective`
`finrank_tensorProduct_adicCompletion_eq_finrank_pi_adicCompletion` 📖	mathematical	—	`TensorProduct.RightActions.instAlgebra_fLT` `Extension` `comap` `comap_pi_algebra`	—	`TensorProduct.finrank_rightAlgebra` `Ideal.sum_ramification_inertia_extensions` `ramification_mul_inertia_eq_finrank_completion` `comap_algebra_finite`
`instIsScalarTowerSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_fLT` 📖	—	—	—	—	—
`instMulActionHomClassAlgHomTensorProductAdicCompletionForallValEqComap` 📖	mathematical	—	`adicCompletion_RkOne` `instAlgebraWithVal_fLT_1` `Extension` `comap`	—	`instIsScalarTowerWithVal_fLT_1`
`instOneHomClassAlgHomTensorProductAdicCompletionForallValEqComap` 📖	mathematical	—	`adicCompletion_RkOne` `instAlgebraWithVal_fLT_1` `Extension` `comap`	—	—
`prodAdicCompletionComap_isModuleTopology` 📖	mathematical	—	`Extension` `comap` `comap_pi_algebra`	—	`adicCompletionComap_isModuleTopology` `Extension.finite`
`prodAdicCompletionsIntegers_eq_closureIntegers` 📖	mathematical	—	`Extension` `comap` `adicCompletionIntegersSubalgebra`	—	`closureAlgebraMapIntegers_eq_prodIntegers`
`ramification_mul_inertia_eq_finrank_completion` 📖	mathematical	`comap`	`comap_algebra`	—	`comap_integer_algebra_finite` `adicCompletion.instIsPrincipalIdealRingSubtypeMemValuationSubringAdicCompletionIntegers_fLT` `completionIdeal_ne_bot` `adicCompletion.ramificationIdx_eq_ramificationIdx` `adicCompletion.inertiaDeg_eq_inertiaDeg`
`tensorAdicCompletionComapAlgHom_bijective` 📖	mathematical	—	`instAlgebraWithVal_fLT_1` `Extension` `comap` `tensorAdicCompletionComapAlgHom`	—	`tensorAdicCompletionComapLinearMap_surjective` `comap_pi_algebra_finite` `finrank_tensorProduct_adicCompletion_eq_finrank_pi_adicCompletion` `TensorProduct.RightActions.instFinite_fLT`
`tensorAdicCompletionComapAlgHom_tmul_apply` 📖	mathematical	—	`instAlgebraWithVal_fLT_1` `Extension` `comap` `tensorAdicCompletionComapAlgHom` `comap_algebra`	—	—
`tensorAdicCompletionComapLinearMap_isOpenQuotientMap` 📖	mathematical	—	`instAlgebraWithVal_fLT_1` `TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT` `Extension` `comap` `TensorProduct.RightActions.instModule_fLT` `comap_pi_algebra` `tensorAdicCompletionComapLinearMap`	—	`IsModuleTopology.t2Space'` `TensorProduct.RightActions.instIsModuleTopology_fLT` `comap_algebra_continuousSmul` `comap_pi_algebra_finite` `tensorAdicCompletionComapLinearMap_surjective` `TensorProduct.RightActions.instFinite_fLT`
`tensorAdicCompletionComapLinearMap_surjective` 📖	mathematical	—	`instAlgebraWithVal_fLT_1` `Extension` `comap` `TensorProduct.RightActions.instModule_fLT` `comap_pi_algebra` `tensorAdicCompletionComapLinearMap`	—	`comap_algebra_continuousSmul` `TensorProduct.RightActions.instFinite_fLT` `Extension.finite` `denseRange_of_prodAlgebraMap` `SemialgHom.baseChangeRightOfAlgebraMap_apply` `SemialgHom.baseChange_of_algebraMap_tmul_left`
`tensorAdicCompletionIntegersToRange_eq_closureIntegers` 📖	mathematical	—	`adicCompletion_RkOne` `instAlgebraWithVal_fLT_1` `tensorAdicCompletionIntegersTo` `TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT`	—	`tensorAdicCompletionIntegersToRange_subset_closureIntegers` `tensorAdicCompletionIsClopenRange`
`tensorAdicCompletionIntegersToRange_subset_closureIntegers` 📖	mathematical	—	`adicCompletion_RkOne` `instAlgebraWithVal_fLT_1` `tensorAdicCompletionIntegersTo` `TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT`	—	`instIsScalarTowerSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_fLT` `TensorProduct.RightActions.instIsModuleTopology_fLT` `denseRange_of_integerAlgebraMap` `instIsScalarTowerWithVal_fLT_1`
`tensorAdicCompletionIntegersTo_tmul` 📖	mathematical	—	`adicCompletion_RkOne` `instAlgebraWithVal_fLT_1` `tensorAdicCompletionIntegersTo`	—	`instIsScalarTowerSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_fLT`
`tensorAdicCompletionIsClopenRange` 📖	mathematical	—	`adicCompletion_RkOne` `instAlgebraWithVal_fLT_1` `TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT` `tensorAdicCompletionIntegersTo`	—	`TensorProduct.RightActions.instIsScalarTower_fLT` `TensorProduct.RightActions.instIsModuleTopology_fLT` `ContinuousLinearEquiv.restrictScalars_symm_apply` `IsModuleTopology.continuousLinearEquiv_symm_apply` `tensorAdicCompletionIntegersTo_tmul` `Module.Basis.rightBaseChange_apply`
`valued_adicCompletionComap` 📖	mathematical	`comap`	`SemialgHom` `instAlgebraWithVal_fLT` `instFunLike` `adicCompletionComapSemialgHom`	—	`adicCompletionComap_coe` `valuation_comap`

IsDedekindDomain.HeightOneSpectrum.WithZero

Theorems

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

IsDedekindDomain.HeightOneSpectrum.adicCompletion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inertiaDeg_eq_inertiaDeg` 📖	mathematical	`IsDedekindDomain.HeightOneSpectrum.comap`	`IsDedekindDomain.HeightOneSpectrum.completionIdeal` `IsDedekindDomain.HeightOneSpectrum.comap_integer_algebra`	—	`IsDedekindDomain.HeightOneSpectrum.algebraMap_completionIntegers` `IsDedekindDomain.HeightOneSpectrum.comap_integer_algebraMap` `instIsScalarTowerWithVal_fLT_1` `SemialgHom.commutes` `IsDedekindDomain.HeightOneSpectrum.mem_completionIdeal_iff` `IsDedekindDomain.HeightOneSpectrum.valued_adicCompletionComap` `IsDedekindDomain.HeightOneSpectrum.ramificationIdx_ne_zero` `IsDedekindDomain.HeightOneSpectrum.instLiesOverSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersCompletionIdealAsIdeal` `IsDedekindDomain.HeightOneSpectrum.inertiaDeg_asIdeal_completionIdeal`
`ramificationIdx_eq_ramificationIdx` 📖	mathematical	`IsDedekindDomain.HeightOneSpectrum.comap`	`IsDedekindDomain.HeightOneSpectrum.comap_integer_algebra` `IsDedekindDomain.HeightOneSpectrum.completionIdeal`	—	`mem_completionIdeal_pow` `IsDedekindDomain.HeightOneSpectrum.comap_integer_algebraMap` `IsDedekindDomain.HeightOneSpectrum.valued_adicCompletionComap` `IsDedekindDomain.HeightOneSpectrum.WithZero.ofAdd_neg_ofNat_pow` `IsDedekindDomain.HeightOneSpectrum.mem_completionIdeal_iff'` `exists_uniformizer` `IsDedekindDomain.HeightOneSpectrum.mem_completionIdeal_iff`

IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapadicCompletionIntegers` 📖	mathematical	`IsDedekindDomain.HeightOneSpectrum.comap`	`SemialgHom` `instAlgebraWithVal_fLT` `instFunLike` `IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom`	—	`IsDedekindDomain.HeightOneSpectrum.valued_adicCompletionComap` `IsDedekindDomain.HeightOneSpectrum.ramificationIdx_ne_zero`

IsDedekindDomain.HeightOneSpectrum.adicValued

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_algebraMap` 📖	—	`IsDedekindDomain.HeightOneSpectrum.comap`	—	—	`IsDedekindDomain.HeightOneSpectrum.ramificationIdx_ne_zero` `IsDedekindDomain.HeightOneSpectrum.valuation_comap` `instIsScalarTowerWithVal_fLT`

---

← Back to Index