def GaloisRep (K : Type uK) [Field K] (A : Type u_2) [CommRing A] [TopologicalSpace A] (M : Type u_4) [AddCommGroup M] [Module A M] : Type (max uK u_4)

GaloisRep K A M are the A-linear galois reps of a field K on the A-module M.

Equations

• GaloisRep K A M = (Field.absoluteGaloisGroup K →ₜ* Module.End A M)

instance instFunLikeGaloisRepAbsoluteGaloisGroupEnd {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] : FunLike (GaloisRep K A M) (Field.absoluteGaloisGroup K) (Module.End A M)

Equations

• instFunLikeGaloisRepAbsoluteGaloisGroupEnd = ContinuousMonoidHom.instFunLike

instance instMonoidHomClassGaloisRepAbsoluteGaloisGroupEnd {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] : MonoidHomClass (GaloisRep K A M) (Field.absoluteGaloisGroup K) (Module.End A M)

theorem GaloisRep.ext {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] {ρ ρ' : GaloisRep K A M} (H : ∀ (σ : Field.absoluteGaloisGroup K), ρ σ = ρ' σ) : ρ = ρ'

theorem GaloisRep.ext_iff {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] {ρ ρ' : GaloisRep K A M} : ρ = ρ' ↔ ∀ (σ : Field.absoluteGaloisGroup K), ρ σ = ρ' σ

@[reducible, inline]

abbrev GaloisRep.ker {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] (ρ : GaloisRep K A M) : Subgroup (Field.absoluteGaloisGroup K)

The kernel of a galois rep.

Equations

• ρ.ker = ρ.ker

noncomputable def GaloisRep.map {K : Type uK} {L : Type u_1} [Field K] [Field L] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] [NumberField K] (ρ : GaloisRep K A M) (f : K →+* L) : GaloisRep L A M

A field extension induces a map between galois reps. Note that this relies on an arbitrarily chosen embedding of the algebraic closures.

Equations

• ρ.map f = ContinuousMonoidHom.comp ρ (Field.absoluteGaloisGroup.map f)

@[simp]

theorem GaloisRep.ker_map {K : Type uK} {L : Type u_1} [Field K] [Field L] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] [NumberField K] (ρ : GaloisRep K A M) (f : K →+* L) : (ρ.map f).ker = Subgroup.comap (↑(Field.absoluteGaloisGroup.map f)) ρ.ker

@[reducible, inline]

abbrev FramedGaloisRep (K : Type uK) [Field K] (A : Type u_2) [CommRing A] [TopologicalSpace A] (n : Type u_6) : Type (max uK u_2 u_6)

A framed galois rep is a galois rep with a distinguished basis. We implement it by via a galois rep on Aⁿ.

Equations

• FramedGaloisRep K A n = GaloisRep K A (n → A)

@[reducible, inline]

noncomputable abbrev FramedGaloisRep.map {K : Type uK} {L : Type u_1} [Field K] [Field L] {A : Type u_2} [CommRing A] [TopologicalSpace A] {n : Type u_6} [NumberField K] (ρ : FramedGaloisRep K A n) (f : K →+* L) : FramedGaloisRep L A n

A field extension induces a map between framed galois reps. Note that this relies on an arbitrarily chosen embedding of the algebraic closures.

Equations

• ρ.map f = GaloisRep.map ρ f

noncomputable def GaloisRep.conj {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} {N : Type u_5} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] (ρ : GaloisRep K A M) (e : M ≃ₗ[A] N) : GaloisRep K A N

We can conjugate a galois rep by a linear isomorphism on the space.

Equations

• ρ.conj e = (↑(ContinuousAlgEquiv.ofIsModuleTopology (LinearEquiv.algConj A e))).toContinuousMonoidHom.comp ρ

theorem GaloisRep.conj_apply {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} {N : Type u_5} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] (ρ : GaloisRep K A M) (e : M ≃ₗ[A] N) (σ : Field.absoluteGaloisGroup K) : (ρ.conj e) σ = e.conj (ρ σ)

@[simp]

theorem GaloisRep.conj_apply_apply {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} {N : Type u_5} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] (ρ : GaloisRep K A M) (e : M ≃ₗ[A] N) (σ : Field.absoluteGaloisGroup K) (x : N) : ((ρ.conj e) σ) x = e ((ρ σ) (e.symm x))

@[simp]

theorem GaloisRep.map_conj {K : Type uK} {L : Type u_1} [Field K] [Field L] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} {N : Type u_5} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [NumberField K] (ρ : GaloisRep K A M) (e : M ≃ₗ[A] N) (f : K →+* L) : (ρ.conj e).map f = (ρ.map f).conj e

@[simp]

theorem GaloisRep.ker_conj {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} {N : Type u_5} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] (ρ : GaloisRep K A M) (e : M ≃ₗ[A] N) : (ρ.conj e).ker = ρ.ker

noncomputable def GaloisRep.conjEquiv {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} {N : Type u_5} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] (e : M ≃ₗ[A] N) : GaloisRep K A M ≃ GaloisRep K A N

Equivalent modules have equivalent set of galois reps.

Equations

• GaloisRep.conjEquiv e = { toFun := fun (x : GaloisRep K A M) => x.conj e, invFun := fun (x : GaloisRep K A N) => x.conj e.symm, left_inv := ⋯, right_inv := ⋯ }

noncomputable def GaloisRep.frame {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] {n : Type u_6} [Fintype n] (ρ : GaloisRep K A M) (b : Module.Basis n A M) : FramedGaloisRep K A n

Given a basis, we may frame a galois rep into a framed galois rep.

Equations

• ρ.frame b = ρ.conj (b.repr.trans (Finsupp.linearEquivFunOnFinite A A n))

noncomputable def FramedGaloisRep.unframe {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] {n : Type u_6} [Fintype n] (ρ : FramedGaloisRep K A n) (b : Module.Basis n A M) : GaloisRep K A M

Given a basis of M, we may realize a framed galois rep as a galois rep on M.

Equations

• ρ.unframe b = GaloisRep.conj ρ (b.repr.trans (Finsupp.linearEquivFunOnFinite A A n)).symm

@[simp]

theorem GaloisRep.unframe_frame {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] {n : Type u_6} [Fintype n] (ρ : GaloisRep K A M) (b : Module.Basis n A M) : (ρ.frame b).unframe b = ρ

@[simp]

theorem FramedGaloisRep.unframe_frame {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] {n : Type u_6} [Fintype n] (ρ : FramedGaloisRep K A n) (b : Module.Basis n A M) : (ρ.unframe b).frame b = ρ

noncomputable def FramedGaloisRep.GL {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {n : Type u_6} [Fintype n] [DecidableEq n] [IsTopologicalRing A] : FramedGaloisRep K A n ≃ (Field.absoluteGaloisGroup K →ₜ* GL n A)

A-linear framed galois reps are equivalent to continuous homomorphisms into GLₙ(A).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FramedGaloisRep.GL_apply {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {n : Type u_6} [Fintype n] [DecidableEq n] [IsTopologicalRing A] (ρ : FramedGaloisRep K A n) (σ : Field.absoluteGaloisGroup K) : ↑((«GL» ρ) σ) = LinearMap.toMatrix' (ρ σ)

@[reducible, inline]

noncomputable abbrev FramedGaloisRep.ofGL {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {n : Type u_6} [Fintype n] [DecidableEq n] [IsTopologicalRing A] : (Field.absoluteGaloisGroup K →ₜ* GL n A) ≃ FramedGaloisRep K A n

Make an A-linear framed galois reps from a continuous hom into GLₙ(A).

Equations

• FramedGaloisRep.ofGL = FramedGaloisRep.GL.symm

@[simp]

theorem FramedGaloisRep.GL_symm_apply {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {n : Type u_6} [Fintype n] [DecidableEq n] [IsTopologicalRing A] (ρ : Field.absoluteGaloisGroup K →ₜ* GL n A) (σ : Field.absoluteGaloisGroup K) : («GL».symm ρ) σ = ↑(Matrix.GeneralLinearGroup.toLin (ρ σ))

@[simp]

theorem FramedGaloisRep.ofGL_apply {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {n : Type u_6} [Fintype n] [DecidableEq n] [IsTopologicalRing A] (ρ : Field.absoluteGaloisGroup K →ₜ* GL n A) (σ : Field.absoluteGaloisGroup K) : (ofGL ρ) σ = ↑(Matrix.GeneralLinearGroup.toLin (ρ σ))

def FramedGaloisRep.equivChar {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {n : Type u_7} [Unique n] : FramedGaloisRep K A n ≃ (Field.absoluteGaloisGroup K →ₜ* A)

1-dimensional framed galois reps are equivalent to (continuous) characters.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GaloisRep.det {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] [IsTopologicalRing A] (ρ : GaloisRep K A M) : Field.absoluteGaloisGroup K →ₜ* A

The determinant of a galois rep.

Equations

• ρ.det = { toMonoidHom := LinearMap.det, continuous_toFun := ⋯ }.comp ρ

noncomputable def GaloisRep.baseChange {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] (B : Type u_3) [CommRing B] [TopologicalSpace B] {M : Type u_4} [AddCommGroup M] [Module A M] [IsTopologicalRing B] [Algebra A B] [ContinuousSMul A B] [Module.Finite A M] [Module.Free A M] (ρ : GaloisRep K A M) : GaloisRep K B (TensorProduct A B M)

Make a A-linear galois rep on M into a B-linear rep on B ⊗ M.

Equations

• GaloisRep.baseChange B ρ = { toMonoidHom := ↑↑(Module.End.baseChangeHom A B M), continuous_toFun := ⋯ }.comp ρ

@[simp]

theorem GaloisRep.baseChange_tmul {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {B : Type u_3} [CommRing B] [TopologicalSpace B] {M : Type u_4} [AddCommGroup M] [Module A M] [IsTopologicalRing B] [Algebra A B] [ContinuousSMul A B] [Module.Finite A M] [Module.Free A M] (ρ : GaloisRep K A M) (σ : Field.absoluteGaloisGroup K) (r : B) (x : M) : ((baseChange B ρ) σ) (r ⊗ₜ[A] x) = r ⊗ₜ[A] (ρ σ) x

theorem GaloisRep.ker_baseChange {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {B : Type u_3} [CommRing B] [TopologicalSpace B] {M : Type u_4} [AddCommGroup M] [Module A M] [IsTopologicalRing B] [Algebra A B] [ContinuousSMul A B] [Module.Finite A M] [Module.Free A M] (ρ : GaloisRep K A M) : ρ.ker ≤ (baseChange B ρ).ker

theorem GaloisRep.baseChange_map {K : Type uK} {L : Type u_1} [Field K] [Field L] {A : Type u_2} [CommRing A] [TopologicalSpace A] {B : Type u_3} [CommRing B] [TopologicalSpace B] {M : Type u_4} [AddCommGroup M] [Module A M] [NumberField K] [IsTopologicalRing B] [Algebra A B] [ContinuousSMul A B] [Module.Finite A M] [Module.Free A M] (ρ : GaloisRep K A M) (f : K →+* L) : (baseChange B ρ).map f = baseChange B (ρ.map f)

noncomputable def FramedGaloisRep.baseChange {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {B : Type u_3} [CommRing B] [TopologicalSpace B] {n : Type u_6} [Fintype n] [DecidableEq n] [IsTopologicalRing A] [IsTopologicalRing B] (ρ : FramedGaloisRep K A n) (f : A →+* B) (hf : Continuous ⇑f) : FramedGaloisRep K B n

Make a framed n dimensional A-linear galois rep into a B-linear rep by composing with GLₙ(A) → GLₙ(B).

Equations

• ρ.baseChange f hf = FramedGaloisRep.ofGL ((Units.mapₜ { toMonoidHom := ↑f.mapMatrix, continuous_toFun := ⋯ }).comp (FramedGaloisRep.GL ρ))

@[simp]

theorem FramedGaloisRep.baseChange_GL {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {B : Type u_3} [CommRing B] [TopologicalSpace B] {n : Type u_6} [Fintype n] [DecidableEq n] [IsTopologicalRing A] [IsTopologicalRing B] (ρ : FramedGaloisRep K A n) (f : A →+* B) (hf : Continuous ⇑f) {σ : Field.absoluteGaloisGroup K} {i j : n} : ↑((«GL» (ρ.baseChange f hf)) σ) i j = f (↑((«GL» ρ) σ) i j)

theorem GaloisRep.frame_baseChange {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] (B : Type u_3) [CommRing B] [TopologicalSpace B] {M : Type u_4} [AddCommGroup M] [Module A M] {n : Type u_6} [Fintype n] [DecidableEq n] [IsTopologicalRing A] [IsTopologicalRing B] [Algebra A B] [ContinuousSMul A B] [Module.Finite A M] [Module.Free A M] (ρ : GaloisRep K A M) (b : Module.Basis n A M) : (baseChange B ρ).frame (Module.Basis.baseChange B b) = (ρ.frame b).baseChange (algebraMap A B) ⋯

theorem FramedGaloisRep.baseChange_def {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {B : Type u_3} [CommRing B] [TopologicalSpace B] {n : Type u_6} [Fintype n] [DecidableEq n] [IsTopologicalRing A] [IsTopologicalRing B] (ρ : FramedGaloisRep K A n) (f : A →+* B) (hf : Continuous ⇑f) : ρ.baseChange f hf = (GaloisRep.baseChange B ρ).frame (Module.Basis.baseChange B (Pi.basisFun A n))

theorem FramedGaloisRep.baseChange_map {K : Type uK} {L : Type u_1} [Field K] [Field L] {A : Type u_2} [CommRing A] [TopologicalSpace A] {B : Type u_3} [CommRing B] [TopologicalSpace B] {n : Type u_6} [Fintype n] [DecidableEq n] [NumberField K] [IsTopologicalRing A] [IsTopologicalRing B] (ρ : FramedGaloisRep K A n) (f : A →+* B) (hf : Continuous ⇑f) (g : K →+* L) : (ρ.baseChange f hf).map g = (ρ.map g).baseChange f hf

theorem Matrix.map_det {F : Type u_7} {α : Type u_8} {β : Type u_9} {n : Type u_10} [CommRing β] [CommRing α] [Fintype n] [DecidableEq n] (M : Matrix n n α) (f : F) [FunLike F α β] [RingHomClass F α β] : (M.map ⇑f).det = f M.det

theorem LinearMap.trace_toLin' {R : Type u_7} {n : Type u_8} [CommSemiring R] [DecidableEq n] [Fintype n] (M : Matrix n n R) : (trace R (n → R)) (Matrix.toLin' M) = M.trace

theorem FramedGaloisRep.det_baseChange {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {B : Type u_3} [CommRing B] [TopologicalSpace B] {n : Type u_6} [Fintype n] [DecidableEq n] [IsTopologicalRing A] [IsTopologicalRing B] (ρ : FramedGaloisRep K A n) (f : A →+* B) (hf : Continuous ⇑f) : GaloisRep.det (ρ.baseChange f hf) = { toMonoidHom := ↑f, continuous_toFun := hf }.comp (GaloisRep.det ρ)

@[reducible, inline]

noncomputable abbrev GaloisRep.toLocal {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] [NumberField K] (ρ : GaloisRep K A M) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : GaloisRep (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) A M

Given a (global) galois rep, this is the local galois rep at a finite prime v. Note: this fixes an arbitrary embedding Kᵃˡᵍ → Kᵥᵃˡᵍ, or equivalently, an arbitrary choice of valuation on Kᵃˡᵍ extending v.

Equations

• ρ.toLocal v = ρ.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))

class GaloisRep.IsUnramifiedAt {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] [NumberField K] (ρ : GaloisRep K A M) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Prop

The class of galois reps unramified at v.

• localInertiaGroup_le : localInertiaGroup v ≤ (ρ.toLocal v).ker

instance instIsUnramifiedAtConj {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} {N : Type u_5} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [NumberField K] (ρ : GaloisRep K A M) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) [ρ.IsUnramifiedAt v] (e : M ≃ₗ[A] N) : (ρ.conj e).IsUnramifiedAt v

instance instIsUnramifiedAtTensorProductBaseChange {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {B : Type u_3} [CommRing B] [TopologicalSpace B] {M : Type u_4} [AddCommGroup M] [Module A M] [NumberField K] [IsTopologicalRing B] [Algebra A B] [ContinuousSMul A B] [Module.Finite A M] [Module.Free A M] (ρ : GaloisRep K A M) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) [ρ.IsUnramifiedAt v] : (GaloisRep.baseChange B ρ).IsUnramifiedAt v

noncomputable def GaloisRep.charFrob {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) [Module.Free A M] [Module.Finite A M] (ρ : GaloisRep K A M) : Polynomial A

The characteristic polynomial of the frobenious conjugacy class at v under ρ.

Equations

• GaloisRep.charFrob v ρ = LinearMap.charpoly ((ρ.toLocal v) (Field.AbsoluteGaloisGroup.adicArithFrob v))

theorem GaloisRep.charFrob_eq {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) [Module.Free A M] [Module.Finite A M] (ρ : GaloisRep K A M) [ρ.IsUnramifiedAt v] (σ : Field.absoluteGaloisGroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (hσ : IsArithFrobAt (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) σ (IsLocalRing.maximalIdeal (IntegralClosure (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (AlgebraicClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))))) : LinearMap.charpoly ((ρ.toLocal v) σ) = charFrob v ρ

def GaloisRep.Space {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] (ρ : GaloisRep K A M) : Type u_4

The underlying space of a galois rep. This is a type class synonym that allows G to act on it via ρ.

Equations

• ρ.Space = M

instance instAddCommGroupSpace {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] (ρ : GaloisRep K A M) : AddCommGroup ρ.Space

Equations

• instAddCommGroupSpace ρ = inferInstance

instance instDistribMulActionAbsoluteGaloisGroupSpace {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] (ρ : GaloisRep K A M) : DistribMulAction (Field.absoluteGaloisGroup K) ρ.Space

Equations

• instDistribMulActionAbsoluteGaloisGroupSpace ρ = { smul := fun (g : Field.absoluteGaloisGroup K) (v : ρ.Space) => (ρ g) v, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

def GaloisRep.HasFlatProlongationAt {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (ρ : GaloisRep K A M) : Prop

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 aformentioned result as a sorry.

Equations

• One or more equations did not get rendered due to their size.

class GaloisRep.IsFlatAt {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) [IsTopologicalRing A] [Module.Free A M] [Module.Finite A M] [IsLocalRing A] (ρ : GaloisRep K A M) : Prop

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.

• cond (I : Ideal A) : IsOpen ↑I → HasFlatProlongationAt v (baseChange (A ⧸ I) ρ)

def GaloisRep.toRepresentation {K : Type uK} [Field K] {A : Type u_2} [CommRing A] [TopologicalSpace A] {M : Type u_4} [AddCommGroup M] [Module A M] (ρ : GaloisRep K A M) : Representation A (Field.absoluteGaloisGroup K) M

A Galois representation is a representation (note that we are forgetting topological information here).

Equations

• ρ.toRepresentation = ρ.toMonoidHom

def GaloisRep.IsIrreducible {K : Type uK} [Field K] {M : Type u_4} [AddCommGroup M] {k : Type u_7} [Field k] [TopologicalSpace k] [Module k M] (ρ : GaloisRep K k M) : Prop

Irreducibility of a Galois representation over a field.

Equations

• ρ.IsIrreducible = ρ.toRepresentation.IsIrreducible