Documentation Verification Report

AbsoluteGaloisGroup

📁 Source: FLT/Deformations/RepresentationTheory/AbsoluteGaloisGroup.lean

Statistics

Metric	Count
Definitions `adicArithFrob`, `map`, `mapAux`, `instNontriviallyNormedFieldAdicCompletionRingOfIntegers_fLT`, `localInertiaGroup`, `localTameAbelianInertiaGroup`	6
Theorems `isArithFrobAt_adicArithFrob`, `lift_map`, `finiteIndex_fixingSubgroup`, `finite_adicCompletionIntegers_quotient`, `instCharZeroAdicCompletionRingOfIntegers_fLT`, `instCompactSpaceAlgEquivOfIsAlgebraic_fLT`, `instContinuousSMulDiscreteAlgEquivOfIsAlgebraic`, `instFiniteResidueFieldSubtypeAdicCompletionRingOfIntegersMemValuationSubringAdicCompletionIntegers_fLT`, `instIsInvariantAlgEquivOfIsGalois_fLT`, `instIsInvariantAlgEquivOfIsGalois_fLT_1`, `isIntegral_of_spectralNorm_le_one`, `neZero_maximalIdeal_integralClosure`, `spectralNorm_inv`, `valuationRing_integralClosure`	14
Total	20

Field.AbsoluteGaloisGroup

Definitions

Name	Category	Theorems
`adicArithFrob` 📖	CompOp	2 math math: `isArithFrobAt_adicArithFrob`, `GaloisRepresentation.IsHardlyRamified.three_adic`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isArithFrobAt_adicArithFrob` 📖	mathematical	—	`IntegralClosure` `instAlgebraSubtypeMemValuationSubring_fLT` `instCommRingIntegralClosure` `instAlgebraIntegralClosure` `mulSemiringActionIntegralClosure` `ValuationSubring.smulCommClass` `smulCommClass_integralClosure` `adicArithFrob` `instIsDomainIntegralClosure` `valuationRing_integralClosure`	—	`IsArithFrobAt.arithFrobAt'` `ValuationSubring.smulCommClass` `smulCommClass_integralClosure` `instIsDomainIntegralClosure` `valuationRing_integralClosure` `instCompactSpaceAlgEquivOfIsAlgebraic_fLT` `isInvariant_integralClosure` `instIsInvariantAlgEquivOfIsGalois_fLT_1` `instCharZeroAdicCompletionRingOfIntegers_fLT` `continuousSMulDiscrete_integralClosure` `instContinuousSMulDiscreteAlgEquivOfIsAlgebraic` `finite_adicCompletionIntegers_quotient` `instNeZeroIdealUnderOfNontrivialOfIsDomainOfIsIntegral_fLT` `instIsIntegralIntegralClosure` `neZero_maximalIdeal_integralClosure`

Field.absoluteGaloisGroup

Definitions

Name	Category	Theorems
`map` 📖	CompOp	2 math math: `GaloisRep.ker_map`, `lift_map`
`mapAux` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lift_map` 📖	mathematical	—	`AlgebraicClosure.map` `map`	—	—

(root)

Definitions

Name	Category	Theorems
`instNontriviallyNormedFieldAdicCompletionRingOfIntegers_fLT` 📖	CompOp	—
`localInertiaGroup` 📖	CompOp	1 math math: `GaloisRep.IsUnramifiedAt.localInertiaGroup_le`
`localTameAbelianInertiaGroup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finiteIndex_fixingSubgroup` 📖	—	—	—	—	—
`finite_adicCompletionIntegers_quotient` 📖	—	—	—	—	`instFiniteResidueFieldSubtypeAdicCompletionRingOfIntegersMemValuationSubringAdicCompletionIntegers_fLT`
`instCharZeroAdicCompletionRingOfIntegers_fLT` 📖	—	—	—	—	—
`instCompactSpaceAlgEquivOfIsAlgebraic_fLT` 📖	—	—	—	—	`IsTopologicalGroup.totallyBounded` `finiteIndex_fixingSubgroup`
`instContinuousSMulDiscreteAlgEquivOfIsAlgebraic` 📖	mathematical	—	`ContinuousSMulDiscrete`	—	—
`instFiniteResidueFieldSubtypeAdicCompletionRingOfIntegersMemValuationSubringAdicCompletionIntegers_fLT` 📖	—	—	—	—	`NumberField.instFiniteResidueFieldAdicCompletionIntegers`
`instIsInvariantAlgEquivOfIsGalois_fLT` 📖	—	—	—	—	—
`instIsInvariantAlgEquivOfIsGalois_fLT_1` 📖	—	—	—	—	—
`isIntegral_of_spectralNorm_le_one` 📖	—	—	—	—	`Subring.algebraMap_def`
`neZero_maximalIdeal_integralClosure` 📖	mathematical	—	`IntegralClosure` `instAlgebraSubtypeMemValuationSubring_fLT` `instCommRingIntegralClosure` `instIsDomainIntegralClosure` `valuationRing_integralClosure`	—	`instIsDomainIntegralClosure` `valuationRing_integralClosure` `not_isField_integralClosure`
`spectralNorm_inv` 📖	—	—	—	—	—
`valuationRing_integralClosure` 📖	mathematical	—	`IntegralClosure` `instAlgebraSubtypeMemValuationSubring_fLT` `instCommRingIntegralClosure` `instIsDomainIntegralClosure`	—	`isIntegral_of_spectralNorm_le_one` `spectralNorm_inv`

---

← Back to Index