Documentation Verification Report

GaloisRep

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

Statistics

Metric	Count
Definitions `FramedGaloisRep`, `GL`, `baseChange`, `equivChar`, `map`, `ofGL`, `unframe`, `GaloisRep`, `HasFlatProlongationAt`, `IsFlatAt`, `IsIrreducible`, `IsUnramifiedAt`, `Space`, `baseChange`, `charFrob`, `conj`, `conjEquiv`, `det`, `frame`, `ker`, `map`, `toLocal`, `toRepresentation`, `instAddCommGroupSpace`, `instDistribMulActionAbsoluteGaloisGroupSpace`, `instFunLikeGaloisRepAbsoluteGaloisGroupEnd`	26
Theorems `GL_apply`, `GL_symm_apply`, `baseChange_GL`, `baseChange_def`, `baseChange_map`, `det_baseChange`, `ofGL_apply`, `unframe_frame`, `cond`, `localInertiaGroup_le`, `baseChange_map`, `baseChange_tmul`, `charFrob_eq`, `conj_apply`, `conj_apply_apply`, `ext`, `ext_iff`, `frame_baseChange`, `ker_baseChange`, `ker_conj`, `ker_map`, `map_conj`, `unframe_frame`, `trace_toLin'`, `map_det`, `instIsUnramifiedAtConj`, `instIsUnramifiedAtTensorProductBaseChange`, `instMonoidHomClassGaloisRepAbsoluteGaloisGroupEnd`	28
Total	54

FramedGaloisRep

Definitions

Name	Category	Theorems
`GL` 📖	CompOp	3 math math: `GL_apply`, `GL_symm_apply`, `baseChange_GL`
`baseChange` 📖	CompOp	6 math math: `baseChange_def`, `baseChange_map`, `baseChange_GL`, `GaloisRep.frame_baseChange`, `det_baseChange`, `Deformation.toFramedGaloisRep_map`
`equivChar` 📖	CompOp	—
`map` 📖	CompOp	1 math math: `baseChange_map`
`ofGL` 📖	CompOp	1 math math: `ofGL_apply`
`unframe` 📖	CompOp	2 math math: `GaloisRep.unframe_frame`, `unframe_frame`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`GL_apply` 📖	mathematical	—	`FramedGaloisRep` `GL` `instFunLikeGaloisRepAbsoluteGaloisGroupEnd`	—	—
`GL_symm_apply` 📖	mathematical	—	`FramedGaloisRep` `instFunLikeGaloisRepAbsoluteGaloisGroupEnd` `GL`	—	—
`baseChange_GL` 📖	mathematical	—	`FramedGaloisRep` `GL` `baseChange`	—	—
`baseChange_def` 📖	mathematical	—	`baseChange` `GaloisRep.frame` `GaloisRep.baseChange`	—	`GaloisRep.frame_baseChange`
`baseChange_map` 📖	mathematical	—	`map` `baseChange`	—	—
`det_baseChange` 📖	mathematical	—	`GaloisRep.det` `baseChange`	—	`GL_symm_apply` `Matrix.map_det`
`ofGL_apply` 📖	mathematical	—	`FramedGaloisRep` `instFunLikeGaloisRepAbsoluteGaloisGroupEnd` `ofGL`	—	—
`unframe_frame` 📖	mathematical	—	`GaloisRep.frame` `unframe`	—	`GaloisRep.ext`

GaloisRep

Definitions

Name	Category	Theorems
`HasFlatProlongationAt` 📖	MathDef	1 math math: `IsFlatAt.cond`
`IsFlatAt` 📖	CompData	1 math math: `GaloisRepresentation.IsHardlyRamified.isFlat`
`IsIrreducible` 📖	MathDef	3 math math: `Mazur_Frey`, `Wiles_Frey`, `FreyCurve.torsion_not_isIrreducible`
`IsUnramifiedAt` 📖	CompData	3 math math: `GaloisRepresentation.IsHardlyRamified.isUnramified`, `instIsUnramifiedAtConj`, `instIsUnramifiedAtTensorProductBaseChange`
`Space` 📖	CompOp	—
`baseChange` 📖	CompOp	9 math math: `ker_baseChange`, `IsFlatAt.cond`, `FramedGaloisRep.baseChange_def`, `baseChange_map`, `baseChange_tmul`, `frame_baseChange`, `GaloisRepresentation.IsHardlyRamified.mem_isCompatible`, `GaloisRepresentation.IsHardlyRamified.lifts`, `instIsUnramifiedAtTensorProductBaseChange`
`charFrob` 📖	CompOp	1 math math: `charFrob_eq`
`conj` 📖	CompOp	7 math math: `map_conj`, `conj_apply_apply`, `conj_apply`, `instIsUnramifiedAtConj`, `GaloisRepresentation.IsHardlyRamified.mem_isCompatible`, `GaloisRepresentation.IsHardlyRamified.lifts`, `ker_conj`
`conjEquiv` 📖	CompOp	—
`det` 📖	CompOp	2 math math: `FramedGaloisRep.det_baseChange`, `GaloisRepresentation.IsHardlyRamified.det`
`frame` 📖	CompOp	4 math math: `FramedGaloisRep.baseChange_def`, `unframe_frame`, `FramedGaloisRep.unframe_frame`, `frame_baseChange`
`ker` 📖	CompOp	5 math math: `ker_baseChange`, `GaloisRepresentation.IsHardlyRamified.isTameAtTwo`, `ker_map`, `IsUnramifiedAt.localInertiaGroup_le`, `ker_conj`
`map` 📖	CompOp	5 math math: `baseChange_map`, `map_conj`, `GaloisRepresentation.IsHardlyRamified.isTameAtTwo`, `ker_map`, `cyclic_base_change`
`toLocal` 📖	CompOp	3 math math: `IsUnramifiedAt.localInertiaGroup_le`, `charFrob_eq`, `GaloisRepresentation.IsHardlyRamified.three_adic`
`toRepresentation` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baseChange_map` 📖	mathematical	—	`map` `baseChange`	—	—
`baseChange_tmul` 📖	mathematical	—	`GaloisRep` `instFunLikeGaloisRepAbsoluteGaloisGroupEnd` `baseChange`	—	—
`charFrob_eq` 📖	mathematical	`IntegralClosure` `instAlgebraSubtypeMemValuationSubring_fLT` `instCommRingIntegralClosure` `instAlgebraIntegralClosure` `mulSemiringActionIntegralClosure` `smulCommClass_integralClosure` `instIsDomainIntegralClosure` `valuationRing_integralClosure`	`GaloisRep` `instFunLikeGaloisRepAbsoluteGaloisGroupEnd` `toLocal` `charFrob`	—	`smulCommClass_integralClosure` `instIsDomainIntegralClosure` `valuationRing_integralClosure` `IsUnramifiedAt.localInertiaGroup_le` `Field.AbsoluteGaloisGroup.isArithFrobAt_adicArithFrob` `charFrob.eq_1`
`conj_apply` 📖	mathematical	—	`GaloisRep` `instFunLikeGaloisRepAbsoluteGaloisGroupEnd` `conj`	—	—
`conj_apply_apply` 📖	mathematical	—	`GaloisRep` `instFunLikeGaloisRepAbsoluteGaloisGroupEnd` `conj`	—	—
`ext` 📖	—	`GaloisRep` `instFunLikeGaloisRepAbsoluteGaloisGroupEnd`	—	—	—
`ext_iff` 📖	mathematical	—	`GaloisRep` `instFunLikeGaloisRepAbsoluteGaloisGroupEnd`	—	`ext`
`frame_baseChange` 📖	mathematical	—	`frame` `baseChange` `FramedGaloisRep.baseChange`	—	`FramedGaloisRep.baseChange_GL`
`ker_baseChange` 📖	mathematical	—	`ker` `baseChange`	—	—
`ker_conj` 📖	mathematical	—	`ker` `conj`	—	—
`ker_map` 📖	mathematical	—	`ker` `map` `Field.absoluteGaloisGroup.map`	—	—
`map_conj` 📖	mathematical	—	`map` `conj`	—	—
`unframe_frame` 📖	mathematical	—	`FramedGaloisRep.unframe` `frame`	—	`ext`

GaloisRep.IsFlatAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cond` 📖	mathematical	—	`GaloisRep.HasFlatProlongationAt` `GaloisRep.baseChange`	—	—

GaloisRep.IsUnramifiedAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`localInertiaGroup_le` 📖	mathematical	—	`localInertiaGroup` `GaloisRep.ker` `GaloisRep.toLocal`	—	—

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trace_toLin'` 📖	—	—	—	—	—

Matrix

Theorems

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

(root)

Definitions

Name	Category	Theorems
`FramedGaloisRep` 📖	CompOp	4 math math: `FramedGaloisRep.GL_apply`, `FramedGaloisRep.GL_symm_apply`, `FramedGaloisRep.baseChange_GL`, `FramedGaloisRep.ofGL_apply`
`GaloisRep` 📖	CompOp	9 math math: `GaloisRepresentation.IsHardlyRamified.mod_three`, `GaloisRepresentation.IsHardlyRamified.isTameAtTwo`, `GaloisRep.baseChange_tmul`, `GaloisRep.conj_apply_apply`, `GaloisRep.ext_iff`, `GaloisRep.conj_apply`, `GaloisRep.charFrob_eq`, `instMonoidHomClassGaloisRepAbsoluteGaloisGroupEnd`, `GaloisRepresentation.IsHardlyRamified.three_adic`
`instAddCommGroupSpace` 📖	CompOp	—
`instDistribMulActionAbsoluteGaloisGroupSpace` 📖	CompOp	—
`instFunLikeGaloisRepAbsoluteGaloisGroupEnd` 📖	CompOp	12 math math: `FramedGaloisRep.GL_apply`, `GaloisRepresentation.IsHardlyRamified.mod_three`, `GaloisRepresentation.IsHardlyRamified.isTameAtTwo`, `GaloisRep.baseChange_tmul`, `GaloisRep.conj_apply_apply`, `FramedGaloisRep.GL_symm_apply`, `GaloisRep.ext_iff`, `GaloisRep.conj_apply`, `GaloisRep.charFrob_eq`, `FramedGaloisRep.ofGL_apply`, `instMonoidHomClassGaloisRepAbsoluteGaloisGroupEnd`, `GaloisRepresentation.IsHardlyRamified.three_adic`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsUnramifiedAtConj` 📖	mathematical	—	`GaloisRep.IsUnramifiedAt` `GaloisRep.conj`	—	`GaloisRep.IsUnramifiedAt.localInertiaGroup_le` `GaloisRep.ker_conj`
`instIsUnramifiedAtTensorProductBaseChange` 📖	mathematical	—	`GaloisRep.IsUnramifiedAt` `GaloisRep.baseChange`	—	`GaloisRep.IsUnramifiedAt.localInertiaGroup_le` `GaloisRep.ker_baseChange`
`instMonoidHomClassGaloisRepAbsoluteGaloisGroupEnd` 📖	mathematical	—	`GaloisRep` `instFunLikeGaloisRepAbsoluteGaloisGroupEnd`	—	—

---

← Back to Index