Documentation Verification Report

BaseChange

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

Statistics

Metric	Count
Definitions `algebra`, `baseChangeAdeleAlgEquiv`, `baseChangeAdeleContinuousAlgEquiv`, `baseChangeAlgEquiv`, `baseChangeContinuousAlgEquiv`, `baseChangeLinearEquiv`, `mapRingHom`, `mapSemialgHom`, `restrictedProduct_pi_equiv`, `restrictedProduct_prod_equiv`, `restrictedProduct_tensorProduct_equiv_restrictedProduct_prod`, `tensorEquivRestrictedProduct`, `tensorEquivTensor`, `baseChangeAlgebra`, `baseChangeIntegerAlgebra`, `instModuleFiniteAdeleRingRestrictedProductHeightOneSpectrumForallAdicCompletionValEqComapCoeSubmoduleSubtypeMemValuationSubringAdicCompletionIntegersPiAdicIntegerSubmoduleCofinite`, `instModuleSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersForallValHeightOneSpectrumEqComap`, `instModuleSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_fLT`, `instMulActionSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_fLT`, `instSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersForallValHeightOneSpectrumEqComap`, `instSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_fLT`, `piAdicIntegerSubmodule`	22
Theorems `algebraMap_apply`, `baseChangeLinearEquiv_tmul`, `baseChange_bijective`, `mapSemialgHom_apply`, `mapSemialgHom_continuous`, `restrictedProduct_pi_isModuleTopology`, `restrictedProduct_prod_equiv_apply`, `restrictedProduct_tensorProduct_equiv_restrictedProduct_prod_apply`, `tensorEquivRestrictedProduct_tmul`, `tensorEquivTensor_tmul`, `algebraMap_apply`, `cofinite_mapsTo_adicCompletionComapSemialgHom`, `instFiniteFiniteAdeleRing_fLT`, `instIsModuleTopologyFiniteAdeleRing_fLT`, `instIsScalarTowerFiniteAdeleRing_fLT`, `instIsScalarTowerFiniteAdeleRing_fLT_1`, `range_adicCompletionTensorIntegerCoe_eq_lTensorRestriction`, `tendsTo_comap_cofinite`	18
Total	40

IsDedekindDomain

Definitions

Name	Category	Theorems
`baseChangeAlgebra` 📖	CompOp	36 math math: `toMatrix_f`, `instLocallyCompactSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT`, `NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_surjective`, `localcomponent_mulLeft`, `FiniteAdeleRing.tensorEquivTensor_tmul`, `instBorelSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT`, `algebraMap_apply`, `basis_eq_single_global`, `NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_equivariant`, `localcomponent_mulRight`, `NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸`, `NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_continuous`, `Rat.FiniteAdeleRing.padicEquiv_bijOn`, `NumberField.AdeleRing.DivisionAlgebra.Aux.smul_D𝔸_prodRight_symm`, `FiniteAdeleRing.baseChangeLinearEquiv_tmul`, `NumberField.AdeleRing.DivisionAlgebra.Aux.instBorelSpaceDf`, `NumberField.AdeleRing.DivisionAlgebra.Aux.instIsModuleTopologyRingOfIntegersProdDinfDf`, `Rat.FiniteAdeleRing.sub_mem_integralAdeles`, `NumberField.FiniteAdeleRing.tensor_isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul`, `instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT`, `NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸_prodRight_units_cont`, `NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸_prodRight_units_aux`, `basis_repr_eq_global`, `NumberField.AdeleRing.DivisionAlgebra.Aux.rest₁_continuous`, `NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸_real_surjective`, `FiniteAdeleRing.Aux.f_commSq`, `NumberField.FiniteAdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul`, `localcomponent_matrix`, `FiniteAdeleRing.Aux.f_g_local_global`, `basis_eq_global`, `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT`, `NumberField.AdeleRing.instBorelSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT`, `instIsScalarTowerFiniteAdeleRing_fLT`, `instIsScalarTowerFiniteAdeleRing_fLT_1`, `NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact`, `NumberField.AdeleRing.DivisionAlgebra.Aux.Uf.spec`
`baseChangeIntegerAlgebra` 📖	CompOp	4 math math: `FiniteAdeleRing.tensorEquivTensor_tmul`, `FiniteAdeleRing.baseChangeLinearEquiv_tmul`, `FiniteAdeleRing.restrictedProduct_prod_equiv_apply`, `FiniteAdeleRing.tensorEquivRestrictedProduct_tmul`
`instModuleFiniteAdeleRingRestrictedProductHeightOneSpectrumForallAdicCompletionValEqComapCoeSubmoduleSubtypeMemValuationSubringAdicCompletionIntegersPiAdicIntegerSubmoduleCofinite` 📖	CompOp	1 math math: `FiniteAdeleRing.restrictedProduct_pi_isModuleTopology`
`instModuleSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersForallValHeightOneSpectrumEqComap` 📖	CompOp	1 math math: `FiniteAdeleRing.restrictedProduct_pi_isModuleTopology`
`instModuleSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_fLT` 📖	CompOp	—
`instMulActionSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_fLT` 📖	CompOp	—
`instSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersForallValHeightOneSpectrumEqComap` 📖	CompOp	—
`instSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_fLT` 📖	CompOp	—
`piAdicIntegerSubmodule` 📖	CompOp	1 math math: `FiniteAdeleRing.restrictedProduct_pi_isModuleTopology`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_apply` 📖	mathematical	—	`baseChangeAlgebra`	—	—
`cofinite_mapsTo_adicCompletionComapSemialgHom` 📖	mathematical	—	`HeightOneSpectrum.comap` `SemialgHom` `instAlgebraWithVal_fLT` `instFunLike` `HeightOneSpectrum.adicCompletionComapSemialgHom`	—	`HeightOneSpectrum.adicCompletionComapSemialgHom.mapadicCompletionIntegers`
`instFiniteFiniteAdeleRing_fLT` 📖	mathematical	—	`BaseChange.algebra`	—	`TensorProduct.RightActions.instFinite_fLT`
`instIsModuleTopologyFiniteAdeleRing_fLT` 📖	mathematical	—	`BaseChange.algebra`	—	`FiniteAdeleRing.restrictedProduct_pi_isModuleTopology`
`instIsScalarTowerFiniteAdeleRing_fLT` 📖	mathematical	—	`baseChangeAlgebra`	—	—
`instIsScalarTowerFiniteAdeleRing_fLT_1` 📖	mathematical	—	`baseChangeAlgebra` `BaseChange.algebra`	—	`SemialgHom.commutes`
`range_adicCompletionTensorIntegerCoe_eq_lTensorRestriction` 📖	mathematical	—	`instAlgebraWithVal_fLT_1` `HeightOneSpectrum.adicCompletionTensorIntegerCoe` `RestrictedProduct.rangeLTensor` `HeightOneSpectrum.integerSubmodule`	—	—
`tendsTo_comap_cofinite` 📖	mathematical	—	`HeightOneSpectrum.comap`	—	`HeightOneSpectrum.Extension.finite`

IsDedekindDomain.BaseChange

Definitions

Name	Category	Theorems
`algebra` 📖	CompOp	5 math math: `IsDedekindDomain.instFiniteFiniteAdeleRing_fLT`, `IsDedekindDomain.FiniteAdeleRing.baseChangeLinearEquiv_tmul`, `IsDedekindDomain.instIsModuleTopologyFiniteAdeleRing_fLT`, `IsDedekindDomain.instIsScalarTowerFiniteAdeleRing_fLT_1`, `algebraMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_apply` 📖	mathematical	—	`algebra` `IsDedekindDomain.HeightOneSpectrum.comap` `IsDedekindDomain.HeightOneSpectrum.comap_algebra`	—	—

IsDedekindDomain.FiniteAdeleRing

Definitions

Name	Category	Theorems
`baseChangeAdeleAlgEquiv` 📖	CompOp	—
`baseChangeAdeleContinuousAlgEquiv` 📖	CompOp	—
`baseChangeAlgEquiv` 📖	CompOp	—
`baseChangeContinuousAlgEquiv` 📖	CompOp	—
`baseChangeLinearEquiv` 📖	CompOp	1 math math: `baseChangeLinearEquiv_tmul`
`mapRingHom` 📖	CompOp	—
`mapSemialgHom` 📖	CompOp	3 math math: `baseChange_bijective`, `mapSemialgHom_continuous`, `mapSemialgHom_apply`
`restrictedProduct_pi_equiv` 📖	CompOp	—
`restrictedProduct_prod_equiv` 📖	CompOp	1 math math: `restrictedProduct_prod_equiv_apply`
`restrictedProduct_tensorProduct_equiv_restrictedProduct_prod` 📖	CompOp	1 math math: `restrictedProduct_tensorProduct_equiv_restrictedProduct_prod_apply`
`tensorEquivRestrictedProduct` 📖	CompOp	1 math math: `tensorEquivRestrictedProduct_tmul`
`tensorEquivTensor` 📖	CompOp	1 math math: `tensorEquivTensor_tmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baseChangeLinearEquiv_tmul` 📖	mathematical	—	`IsDedekindDomain.baseChangeAlgebra` `baseChangeLinearEquiv` `IsDedekindDomain.baseChangeIntegerAlgebra` `IsDedekindDomain.BaseChange.algebra`	—	`tensorEquivTensor_tmul` `IsDedekindDomain.HeightOneSpectrum.adicCompletionComapIntegerLinearEquiv_tmul_apply` `instIsScalarTowerWithVal_fLT_1` `IsDedekindDomain.algebraMap_apply`
`baseChange_bijective` 📖	mathematical	—	`SemialgHom.baseChange_of_algebraMap` `mapSemialgHom`	—	`IsIntegralClosure.isLocalizedModule` `IsLocalization.tensorProduct_ext` `SemialgHom.baseChange_of_algebraMap_tmul` `IsDedekindDomain.algebraMap_apply` `baseChangeLinearEquiv_tmul`
`mapSemialgHom_apply` 📖	mathematical	—	`SemialgHom` `instFunLike` `mapSemialgHom` `IsDedekindDomain.HeightOneSpectrum.comap` `IsDedekindDomain.HeightOneSpectrum.comap_algebra`	—	—
`mapSemialgHom_continuous` 📖	mathematical	—	`SemialgHom` `instFunLike` `mapSemialgHom`	—	`IsDedekindDomain.tendsTo_comap_cofinite` `IsDedekindDomain.cofinite_mapsTo_adicCompletionComapSemialgHom` `IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom_continuous`
`restrictedProduct_pi_isModuleTopology` 📖	mathematical	—	`IsDedekindDomain.HeightOneSpectrum.Extension` `IsDedekindDomain.HeightOneSpectrum.comap` `IsDedekindDomain.instModuleSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersForallValHeightOneSpectrumEqComap` `IsDedekindDomain.piAdicIntegerSubmodule` `IsDedekindDomain.instModuleFiniteAdeleRingRestrictedProductHeightOneSpectrumForallAdicCompletionValEqComapCoeSubmoduleSubtypeMemValuationSubringAdicCompletionIntegersPiAdicIntegerSubmoduleCofinite`	—	`IsDedekindDomain.instFiniteFiniteAdeleRing_fLT` `IsDedekindDomain.HeightOneSpectrum.prodAdicCompletionComap_isModuleTopology` `RestrictedProduct.isModuleTopology` `IsDedekindDomain.HeightOneSpectrum.Extension.finite`
`restrictedProduct_prod_equiv_apply` 📖	mathematical	—	`IsDedekindDomain.HeightOneSpectrum.Extension` `IsDedekindDomain.HeightOneSpectrum.comap` `instAlgebraWithVal_fLT_1` `instIsScalarTowerWithVal_fLT_1` `IsDedekindDomain.HeightOneSpectrum.integerSubmodule` `IsDedekindDomain.baseChangeIntegerAlgebra` `restrictedProduct_prod_equiv`	—	`instIsScalarTowerWithVal_fLT_1`
`restrictedProduct_tensorProduct_equiv_restrictedProduct_prod_apply` 📖	mathematical	—	`IsDedekindDomain.HeightOneSpectrum.Extension` `IsDedekindDomain.HeightOneSpectrum.comap` `instAlgebraWithVal_fLT_1` `instIsScalarTowerWithVal_fLT_1` `IsDedekindDomain.HeightOneSpectrum.integerSubmodule` `RestrictedProduct.rangeLTensor` `restrictedProduct_tensorProduct_equiv_restrictedProduct_prod` `IsDedekindDomain.HeightOneSpectrum.adicCompletionComapIntegerLinearEquiv`	—	`instIsScalarTowerWithVal_fLT_1`
`tensorEquivRestrictedProduct_tmul` 📖	mathematical	—	`instAlgebraWithVal_fLT_1` `RestrictedProduct.rangeLTensor` `IsDedekindDomain.HeightOneSpectrum.integerSubmodule` `IsDedekindDomain.baseChangeIntegerAlgebra` `tensorEquivRestrictedProduct`	—	—
`tensorEquivTensor_tmul` 📖	mathematical	—	`IsDedekindDomain.baseChangeAlgebra` `IsDedekindDomain.baseChangeIntegerAlgebra` `tensorEquivTensor`	—	`IsDedekindDomain.linearEquivTensorProductModule_tmul`

---

← Back to Index