GaloisRep.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

52 declarations, 0 contain sorry, 0 declared as axioms

Galois representations

The type GaloisRep K A M of A-linear continuous representations of the absolute Galois group of a field K on an A-module M, together with the basic API (kernel, etc.).

Imports (7)

Imported by 6 files

def GaloisRep GaloisRep K A M are the A-linear galois reps of a field K on the A-module M line 49 source
Source documentation
GaloisRep K A M are the A-linear galois reps of a field K on the A-module M.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module
Proof uses: ContinuousMonoidHom, Field.absoluteGaloisGroup, Module.End, AlgebraicClosure, moduleTopology, RingHom.id
26 instances, coercions and auxiliary constants left out.
```
def GaloisRep :=
…
```
instance (instance at line 53) line 53 source
instance (instance at line 57) line 57 source
lemma GaloisRep.ext line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, GaloisRep, Field.absoluteGaloisGroup, Eq, Module.End
Proof uses: ContinuousMonoidHom.ext, AlgebraicClosure, moduleTopology, RingHom.id
30 instances, coercions and auxiliary constants left out.
abbrev GaloisRep.ker line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, GaloisRep, Subgroup, Field.absoluteGaloisGroup, AlgebraicClosure
Proof uses: MonoidHom.ker, Module.End, ContinuousMonoidHom.toMonoidHom, moduleTopology, RingHom.id
35 instances, coercions and auxiliary constants left out.
def GaloisRep.map line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, GaloisRep, RingHom
Proof uses: ContinuousMonoidHom.comp, Field.absoluteGaloisGroup, Module.End, AlgebraicClosure, moduleTopology, RingHom.id, Field.absoluteGaloisGroup.map
29 instances, coercions and auxiliary constants left out.
lemma GaloisRep.ker_map line 83 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, GaloisRep, RingHom, Eq, Subgroup, Field.absoluteGaloisGroup, AlgebraicClosure, GaloisRep.ker, GaloisRep.map, Subgroup.comap, ContinuousMonoidHom.toMonoidHom, Field.absoluteGaloisGroup.map
Proof uses: rfl
24 instances, coercions and auxiliary constants left out.
abbrev FramedGaloisRep A framed galois rep is a galois rep with a distinguished basis line 89 source
Source documentation
A framed galois rep is a galois rep with a distinguished basis. We implement it by via a galois rep on Aⁿ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace
Proof uses: GaloisRep
9 instances, coercions and auxiliary constants left out.
```
abbrev FramedGaloisRep := GaloisRep K A (n → A)
…
```
Mentions: GaloisRep
abbrev FramedGaloisRep.map line 94 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, FramedGaloisRep, RingHom
Proof uses: GaloisRep.map
16 instances, coercions and auxiliary constants left out.
def GaloisRep.conj line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, GaloisRep, LinearEquiv, RingHom.id
Proof uses: ContinuousAlgEquiv, Module.End, moduleTopology, ContinuousAlgEquiv.ofIsModuleTopology, LinearEquiv.conjAlgEquiv, ContinuousMonoidHom.comp, Field.absoluteGaloisGroup, AlgebraicClosure, ContinuousAlgHom.toContinuousMonoidHom
36 instances, coercions and auxiliary constants left out.
lemma GaloisRep.conj_apply line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, GaloisRep, LinearEquiv, RingHom.id, Field.absoluteGaloisGroup, Eq, Module.End, GaloisRep.conj, LinearEquiv.conj
Proof uses: rfl
24 instances, coercions and auxiliary constants left out.
lemma GaloisRep.conj_apply_apply line 112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, GaloisRep, LinearEquiv, RingHom.id, Field.absoluteGaloisGroup, Eq, Module.End, GaloisRep.conj, LinearEquiv.symm
Proof uses: rfl
18 instances, coercions and auxiliary constants left out.
lemma GaloisRep.map_conj line 117 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, GaloisRep, LinearEquiv, RingHom.id, RingHom, Eq, GaloisRep.map, GaloisRep.conj
Proof uses: rfl
14 instances, coercions and auxiliary constants left out.
lemma GaloisRep.ker_conj line 123 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, GaloisRep, LinearEquiv, RingHom.id, Eq, Subgroup, Field.absoluteGaloisGroup, AlgebraicClosure, GaloisRep.ker, GaloisRep.conj
Proof uses: Module.End, moduleTopology, Subgroup.ext, of_eq_true, Iff, Membership.mem, Eq.trans, ContinuousMonoidHom, OfNat.ofNat, True, congr, congrArg, MonoidHom.ker, ContinuousMonoidHom.toMonoidHom, ContinuousMonoidHom.comp, ContinuousAlgHom.toContinuousMonoidHom, ContinuousAlgEquiv.ofIsModuleTopology, LinearEquiv.conjAlgEquiv, MonoidHom, ContinuousAlgEquiv and 3 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def GaloisRep.conjEquiv line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, LinearEquiv, RingHom.id, Equiv, GaloisRep
Proof uses: Equiv.mk, GaloisRep.conj, LinearEquiv.symm
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def GaloisRep.frame line 139 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, Fintype, GaloisRep, Module.Basis, FramedGaloisRep
Proof uses: GaloisRep.conj, LinearEquiv.trans, Finsupp, RingHom.id, Module.Basis.repr, Finsupp.linearEquivFunOnFinite
21 instances, coercions and auxiliary constants left out.
def FramedGaloisRep.unframe line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, Fintype, FramedGaloisRep, Module.Basis, GaloisRep
Proof uses: GaloisRep.conj, LinearEquiv.symm, RingHom.id, LinearEquiv.trans, Finsupp, Module.Basis.repr, Finsupp.linearEquivFunOnFinite
22 instances, coercions and auxiliary constants left out.
lemma GaloisRep.unframe_frame line 151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, Fintype, GaloisRep, Module.Basis, Eq, FramedGaloisRep.unframe, GaloisRep.frame
Proof uses: GaloisRep.ext, Field.absoluteGaloisGroup, LinearMap.ext, RingHom.id, Module.End, of_eq_true, LinearMap, Eq.trans, True, congrFun', congrArg, LinearEquiv, LinearEquiv.trans, Finsupp, LinearEquiv.symm, Finsupp.linearEquivFunOnFinite, Module.Basis.repr, GaloisRep.conj, LinearEquiv.symm_apply_apply, eq_self
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma FramedGaloisRep.unframe_frame line 157 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, Fintype, FramedGaloisRep, Module.Basis, Eq, GaloisRep.frame, FramedGaloisRep.unframe
Proof uses: GaloisRep.ext, Field.absoluteGaloisGroup, LinearMap.ext, RingHom.id, GaloisRep, Module.End, funext, LinearMap, of_eq_true, Eq.trans, True, congrFun', congrArg, LinearEquiv, LinearEquiv.trans, Finsupp, Module.Basis.repr, Finsupp.linearEquivFunOnFinite, GaloisRep.conj, LinearEquiv.symm and 6 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def FramedGaloisRep.GL line 166 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, Fintype, DecidableEq, IsTopologicalRing, Equiv, FramedGaloisRep, ContinuousMonoidHom, Field.absoluteGaloisGroup, Matrix.GeneralLinearGroup, AlgebraicClosure, Matrix
Proof uses: Equiv.mk, ContinuousMonoidHom.toHomUnits, ContinuousMonoidHom.comp, Module.End, moduleTopology, RingHom.id, ContinuousAlgHom.toContinuousMonoidHom, ContinuousAlgEquiv.ofIsModuleTopology, LinearMap.toMatrixAlgEquiv', ContinuousAlgEquiv.symm, Units, Units.coeHomₜ
68 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma FramedGaloisRep.GL_apply line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, Fintype, DecidableEq, IsTopologicalRing, FramedGaloisRep, Field.absoluteGaloisGroup, Eq, Matrix, ContinuousMonoidHom, Matrix.GeneralLinearGroup, AlgebraicClosure, Equiv, FramedGaloisRep.GL, LinearEquiv, RingHom.id, LinearMap, LinearMap.toMatrix', Module.End
Proof uses: rfl
73 instances, coercions and auxiliary constants left out.
abbrev FramedGaloisRep.ofGL line 182 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, Fintype, DecidableEq, IsTopologicalRing, Equiv, ContinuousMonoidHom, Field.absoluteGaloisGroup, Matrix.GeneralLinearGroup, AlgebraicClosure, Matrix, FramedGaloisRep
Proof uses: Equiv.symm, FramedGaloisRep.GL
38 instances, coercions and auxiliary constants left out.
lemma FramedGaloisRep.GL_symm_apply line 186 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, Fintype, DecidableEq, IsTopologicalRing, ContinuousMonoidHom, Field.absoluteGaloisGroup, Matrix.GeneralLinearGroup, AlgebraicClosure, Matrix, Eq, Module.End, FramedGaloisRep, Equiv, Equiv.symm, FramedGaloisRep.GL, LinearMap, RingHom.id, MulEquiv and 2 more
Proof uses: rfl
69 instances, coercions and auxiliary constants left out.
lemma FramedGaloisRep.ofGL_apply line 190 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, Fintype, DecidableEq, IsTopologicalRing, ContinuousMonoidHom, Field.absoluteGaloisGroup, Matrix.GeneralLinearGroup, AlgebraicClosure, Matrix, Eq, Module.End, FramedGaloisRep, Equiv, FramedGaloisRep.ofGL, LinearMap, RingHom.id, MulEquiv, LinearMap.GeneralLinearGroup and 1 more
Proof uses: rfl
69 instances, coercions and auxiliary constants left out.
def FramedGaloisRep.equivChar 1-dimensional framed galois reps are equivalent to (continuous) characters line 194 source
Source documentation
1-dimensional framed galois reps are equivalent to (continuous) characters.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, IsTopologicalRing, Unique, Equiv, FramedGaloisRep, ContinuousMonoidHom, Field.absoluteGaloisGroup, AlgebraicClosure
Proof uses: Equiv.mk, ContinuousMonoidHom.comp, Module.End, moduleTopology, RingHom.id, ContinuousAlgHom.toContinuousMonoidHom, ContinuousAlgEquiv.ofIsModuleTopology, AlgEquiv.trans, LinearMap, Matrix, LinearMap.toMatrixAlgEquiv', Matrix.uniqueAlgEquiv, ContinuousAlgEquiv.symm
63 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
noncomputable def FramedGaloisRep.equivChar {n : Type*} [Unique n] :
    FramedGaloisRep K A n ≃ (Γ K →ₜ* A) :=
…
```
Mentions: FramedGaloisRep
def GaloisRep.det line 207 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, IsTopologicalRing, GaloisRep, ContinuousMonoidHom, Field.absoluteGaloisGroup, AlgebraicClosure
Proof uses: ContinuousMonoidHom.comp, LinearMap, RingHom.id, moduleTopology, Module.End, ContinuousMonoidHom.mk, LinearMap.det
43 instances, coercions and auxiliary constants left out.
def GaloisRep.baseChange line 215 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, IsTopologicalRing, Algebra, ContinuousSMul, Module.Finite, Module.Free, GaloisRep, TensorProduct
Proof uses: RingHom, Module.End, AlgHom, Module.End.baseChangeHom, Continuous, moduleTopology, RingHom.id, ContinuousMonoidHom.comp, Field.absoluteGaloisGroup, AlgebraicClosure, ContinuousMonoidHom.mk
75 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma GaloisRep.baseChange_tmul line 234 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, IsTopologicalRing, Algebra, ContinuousSMul, Module.Finite, Module.Free, GaloisRep, Field.absoluteGaloisGroup, Eq, TensorProduct, Module.End, RingHom.id, GaloisRep.baseChange, TensorProduct.tmul
Proof uses: rfl
38 instances, coercions and auxiliary constants left out.
lemma GaloisRep.ker_baseChange line 240 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, IsTopologicalRing, Algebra, ContinuousSMul, Module.Finite, Module.Free, GaloisRep, LE.le, Subgroup, Field.absoluteGaloisGroup, AlgebraicClosure, GaloisRep.ker, TensorProduct, GaloisRep.baseChange
Proof uses: of_eq_true, Membership.mem, MonoidHom.ker, Module.End, ContinuousMonoidHom.toMonoidHom, moduleTopology, RingHom.id, ContinuousMonoidHom.comp, ContinuousMonoidHom.mk, AlgHom, Module.End.baseChangeHom, MonoidHom, RingHom, Continuous, OneHom.toFun, id, Eq, Eq.refl, Eq.trans, OfNat.ofNat and 9 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma GaloisRep.baseChange_map line 246 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, IsTopologicalRing, Algebra, ContinuousSMul, Module.Finite, Module.Free, GaloisRep, RingHom, Eq, TensorProduct, GaloisRep.map, GaloisRep.baseChange
Proof uses: rfl
36 instances, coercions and auxiliary constants left out.
def FramedGaloisRep.baseChange line 253 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, Fintype, DecidableEq, IsTopologicalRing, FramedGaloisRep, RingHom, Continuous
Proof uses: Equiv, ContinuousMonoidHom, Field.absoluteGaloisGroup, Matrix.GeneralLinearGroup, AlgebraicClosure, Matrix, FramedGaloisRep.ofGL, ContinuousMonoidHom.comp, Units, Units.mapₜ, ContinuousMonoidHom.mk, RingHom.mapMatrix, FramedGaloisRep.GL
35 instances, coercions and auxiliary constants left out.
lemma FramedGaloisRep.baseChange_GL line 259 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, Fintype, DecidableEq, IsTopologicalRing, FramedGaloisRep, RingHom, Continuous, Field.absoluteGaloisGroup, Eq, Matrix, ContinuousMonoidHom, Matrix.GeneralLinearGroup, AlgebraicClosure, Equiv, FramedGaloisRep.GL, FramedGaloisRep.baseChange
Proof uses: of_eq_true, LinearMap, RingHom.id, Module.End, Pi.single, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, ContinuousMonoidHom.mk, RingHom.mapMatrix, MonoidHom, OneHom.toFun, id, Eq.refl, Units, Matrix.map, LinearEquiv, LinearMap.toMatrix' and 7 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma GaloisRep.frame_baseChange line 266 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, Fintype, DecidableEq, IsTopologicalRing, Algebra, ContinuousSMul, Module.Finite, Module.Free, GaloisRep, Module.Basis, Eq, FramedGaloisRep, GaloisRep.frame, TensorProduct, GaloisRep.baseChange, Module.Basis.baseChange and 3 more
Proof uses: Equiv.injective, ContinuousMonoidHom, Field.absoluteGaloisGroup, Matrix.GeneralLinearGroup, AlgebraicClosure, Matrix, FramedGaloisRep.GL, ContinuousMonoidHom.ext, Equiv, Units.ext, Matrix.ext, of_eq_true, Eq.trans, RingHom, Finsupp, LinearEquiv, RingHom.id, Module.Basis.repr, Module.End, True and 26 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma FramedGaloisRep.baseChange_def line 276 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, Fintype, DecidableEq, IsTopologicalRing, FramedGaloisRep, RingHom, Continuous, Eq, FramedGaloisRep.baseChange, GaloisRep.frame, TensorProduct, RingHom.toAlgebra, GaloisRep.baseChange, continuousSMul_of_algebraMap, Module.Basis.baseChange, Pi.basisFun
Proof uses: Algebra, ContinuousSMul, Eq.mpr, Algebra.algebraMap, continuous_algebraMap, id, congrArg, GaloisRep.frame_baseChange, Eq.refl
59 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma FramedGaloisRep.baseChange_map line 288 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, Fintype, DecidableEq, IsTopologicalRing, FramedGaloisRep, RingHom, Continuous, Eq, FramedGaloisRep.map, FramedGaloisRep.baseChange
Proof uses: rfl
20 instances, coercions and auxiliary constants left out.
lemma Matrix.map_det line 292 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Fintype, DecidableEq, Matrix, FunLike, RingHomClass, Eq, Matrix.det, Matrix.map
Proof uses: Eq.symm, RingHom, RingHom.mapMatrix, RingHom.map_det
11 instances, coercions and auxiliary constants left out.
lemma LinearMap.trace_toLin' line 298 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommSemiring, DecidableEq, Fintype, Matrix, Eq, LinearMap, RingHom.id, LinearMap.trace, LinearEquiv, Matrix.toLin', Matrix.trace
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Matrix.trace_toLin'_eq, eq_self
56 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma FramedGaloisRep.det_baseChange line 304 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, Fintype, DecidableEq, IsTopologicalRing, FramedGaloisRep, RingHom, Continuous, Eq, ContinuousMonoidHom, Field.absoluteGaloisGroup, AlgebraicClosure, GaloisRep.det, FramedGaloisRep.baseChange, ContinuousMonoidHom.comp, ContinuousMonoidHom.mk
Proof uses: ContinuousMonoidHom.ext, id, Eq.mpr, MonoidHom, LinearMap, RingHom.id, LinearMap.det, moduleTopology, Module.End, Equiv, Matrix.GeneralLinearGroup, Matrix, FramedGaloisRep.ofGL, Units, Units.mapₜ, RingHom.mapMatrix, FramedGaloisRep.GL, MulEquiv, LinearMap.GeneralLinearGroup, Matrix.GeneralLinearGroup.toLin and 20 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
abbrev GaloisRep.toLocal line 316 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, NumberField, GaloisRep, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, IsDedekindDomain.HeightOneSpectrum.adicCompletion
Proof uses: GaloisRep.map, Algebra.algebraMap
20 instances, coercions and auxiliary constants left out.
class GaloisRep.IsUnramifiedAt The class of galois reps unramified at v line 323 source
Source documentation
The class of galois reps unramified at v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, NumberField, GaloisRep, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
class GaloisRep.IsUnramifiedAt (ρ : GaloisRep K A M) (v : Ω K) : Prop where
…
```
Mentions: GaloisRep
instance (instance at line 328) line 328 source
instance (instance at line 332) line 332 source
def GaloisRep.charFrob line 342 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Module.Free, Module.Finite, GaloisRep, Polynomial
Proof uses: LinearMap.charpoly, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Field.absoluteGaloisGroup, Module.End, GaloisRep.toLocal, Field.AbsoluteGaloisGroup.adicArithFrob
14 instances, coercions and auxiliary constants left out.
instance (instance at line 345) line 345 source
Source comment
shortcut instance for next theorem: needed after mathlib #34045
```
noncomputable instance : CommRing Kᵥ := inferInstance
…
```
lemma GaloisRep.charFrob_eq line 349 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Module.Free, Module.Finite, GaloisRep, GaloisRep.IsUnramifiedAt, Field.absoluteGaloisGroup, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsArithFrobAt, Subtype, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, IntegralClosure and 8 more
Proof uses: Subgroup, GaloisRep.ker, HMul.hMul, Inv.inv, Field.AbsoluteGaloisGroup.adicArithFrob, GaloisRep.IsUnramifiedAt.localInertiaGroup_le, IsArithFrobAt.mul_inv_mem_inertia, Field.AbsoluteGaloisGroup.isArithFrobAt_adicArithFrob, MonoidHom, ContinuousMonoidHom.toMonoidHom, moduleTopology, RingHom.id, OfNat.ofNat, id, congrArg, Eq.mpr, ContinuousMonoidHom, Eq.mp, congr, Eq.trans and 4 more
122 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def GaloisRep.Space The underlying space of a galois rep line 365 source
Source documentation
The underlying space of a galois rep. This is a type class synonym that allows G to act on it via ρ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, GaloisRep
6 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
def GaloisRep.Space (ρ : GaloisRep K A M) : Type _ := M
```
Mentions: GaloisRep
instance (instance at line 367) line 367 source

instance (instance at line 371) line 371 source

Source comment

dirty hack

noncomputable instance (ρ : GaloisRep K A M) : DistribMulAction (Γ K) ρ.Space where
…

Mentions: GaloisRep

def GaloisRep.HasFlatProlongationAt Documented declaration: HasFlatProlongationAt line 390 source
Source documentation
A galois rep ρ : Γ K → Aut_A(M) has a flat prolongation at v if M (when viewed as a Γ Kᵥ) module is isomorphic to the geometric points of a finite etale hopf algebra over Kᵥ, and there exists an finite flat hopf algebra over 𝒪ᵥ whose generic fiber is isomorphic to it. In particular this requires M (and by extension A) to have finite cardinality.
Note that the Algebra.Etale Kᵥ (Kᵥ ⊗[𝒪ᵥ] G) condition is redundant because Kᵥ has char 0 and all finite flat group schemes over Kᵥ are etale. But this would be hard to prove in general, while in the applications they would come from finite groups so it would be easy to show that they are etale. If this turns out to not be the case, we can remove this condition and state the aforementioned result as a sorry.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, GaloisRep
Proof uses: Exists, HopfAlgebra, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Module.Flat, Module.Finite, Algebra.Etale, TensorProduct, DistribMulActionHom, Field.absoluteGaloisGroup, AlgebraicClosure, MonoidHom.id, Additive, AlgHom, GaloisRep.Space, GaloisRep.toLocal, Function.Bijective
51 instances, coercions and auxiliary constants left out.
```
def GaloisRep.HasFlatProlongationAt (ρ : GaloisRep K A M) : Prop :=
…
```
Mentions: GaloisRep
class GaloisRep.IsFlatAt A galois rep ρ : Γ K → Aut_A(M) is flat at v if A/I ⊗ M has a flat prolongation at v for all open ideals I line 398 source
Source documentation
A galois rep ρ : Γ K → Aut_A(M) is flat at v if A/I ⊗ M has a flat prolongation at v for all open ideals I.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, IsTopologicalRing, Module.Free, Module.Finite, IsLocalRing, GaloisRep
7 instances, coercions and auxiliary constants left out.
```
class GaloisRep.IsFlatAt [IsLocalRing A] (ρ : GaloisRep K A M) : Prop where
…
```
Mentions: GaloisRep
def GaloisRep.toRepresentation A Galois representation is a representation (note that we are forgetting topological information here) line 406 source
Source documentation
A Galois representation is a representation (note that we are forgetting topological information here).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, TopologicalSpace, AddCommGroup, Module, GaloisRep, Representation, Field.absoluteGaloisGroup, AlgebraicClosure
Proof uses: ContinuousMonoidHom.toMonoidHom, Module.End, moduleTopology, RingHom.id
34 instances, coercions and auxiliary constants left out.
```
def GaloisRep.toRepresentation (ρ : GaloisRep K A M) : Representation A (Γ K) M :=
…
```
Mentions: GaloisRep
def GaloisRep.IsIrreducible Irreducibility of a Galois representation over a field line 411 source
Source documentation
Irreducibility of a Galois representation over a field.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, AddCommGroup, TopologicalSpace, Module, GaloisRep
Proof uses: Representation.IsIrreducible, Field.absoluteGaloisGroup, AlgebraicClosure, GaloisRep.toRepresentation
16 instances, coercions and auxiliary constants left out.
```
def GaloisRep.IsIrreducible {k : Type*} [Field k] [TopologicalSpace k] [Module k M]
    (ρ : GaloisRep K k M) : Prop := ρ.toRepresentation.IsIrreducible
```
Mentions: GaloisRep