Fermat's Last Theorem Blueprint

3. Reducibility Of p-Torsion Of The Frey Curve🔗

3.1. Overview🔗

In the reductions chapter we reduced Fermat's Last Theorem, modulo a hard theorem from the 1970s, to the assertion that p-torsion in the Frey curve is reducible. In this chapter we deduce that assertion from three more complex claims about hardly ramified Galois representations. One of those three claims is comparatively close to Fontaine's work from the 1980s on the nonexistence of nontrivial abelian schemes over \mathbf{Z}. The other two lie deeper and use techniques developed in the 1990s and later around Wiles-style R = T arguments.

3.2. Hardly Ramified Representations🔗

Let (a,b,c,p) be a Frey package, let E be the corresponding Frey curve over \Q, and let \rho : \GQ \to \Aut(E(\Qbar)[p]) be the 2-dimensional Galois representation on the p-torsion of E. Our goal is to prove that \rho is reducible.

What we need to leverage is the fact that \rho has very little ramification. To give a toy example before we start: if K is a number field, that is, a finite extension of \Q, and if the extension K / \Q is unramified at all primes, then an old theorem of Minkowski tells us that K = \Q. We want to prove a theorem in a similar vein, namely that if a 2-dimensional mod p Galois representation is hardly ramified, then it is reducible. Below, we give a precise definition of what it means for a continuous 2-dimensional representation \GQ \to \GL_2(R) to be hardly ramified. Before we do that, we need to say precisely which topological rings R we will allow. We say that a topological ring is pro-Artinian if it is a projective limit of Artin local rings each equipped with the discrete topology, and if it has the projective limit topology. We are only concerned with local pro-Artinian rings with finite residue field; such things can be checked to be the same thing as topological local rings with finite residue field whose underlying topological space is profinite, and such that additive translates of open ideals form a basis for the topology. Let us call such rings coefficient rings for now.

We make some remarks to orient the reader.

  • Any complete local Noetherian ring with finite residue field is a coefficient ring, if the ring is equipped with the \m-adic topology where \m is the maximal ideal. In this case, all powers of \m are open.

  • In particular finite fields, and integer rings of finite extensions of \Q_p, are coefficient rings.

  • If R is a coefficient ring then R is isomorphic to the projective limit of the finite rings R/I as I runs over the open ideals of R.

  • A non-Noetherian example of a coefficient ring is the projective limit over n of the rings \Z/p\Z[\varepsilon_1,\ldots,\varepsilon_n]/(\forall i,j,\varepsilon_i\varepsilon_j=0); these rings are convenient to include as coefficient rings for technical reasons; they make representability theorems easier.

  • The category of coefficient rings is equivalent to the pro-category of the category of finite local rings.

  • A coefficient ring is pseudocompact in the sense of Grothendieck. A pseudocompact local ring is however a more general concept as such a thing may have an infinite residue field and would thus not be profinite.

  • If R is a coefficient ring with residue field of characteristic \ell, then there is a unique continuous map \Z_\ell\to R. Indeed, it suffices to prove that there is a unique continuous map \Z_\ell\to R/I for each open ideal I, but R/I is a finite local ring with residue field of characteristic \ell. R/I is hence Artinian, so some power of the maximal ideal is zero by Nakayama. This means that \ell^N=0 for some sufficiently large N, and hence R/I is a \Z/\ell^N\Z-algebra and thus admits admits a unique map from \Z_\ell.

  • It will be more convenient to fix once and for all the integer \mathcal{O} in a finite extension of \Q_\ell and consider coefficient \mathcal{O}-algebras, namely coefficient rings R equipped with a continuous map \mathcal{O}\to R which is a local homomorphism inducing an isomorphism on residue fields.

Because a coefficient ring with residue characteristic \ell is naturally a \mathbf{Z}_\ell-algebra, we can talk about the \ell-adic cyclotomic character with values in that ring. We are now ready to define hardly ramified representations.

Definition3.1
Group: Reducibility of p -torsion of the Frey curve. (7)
Hover another entry in this group to preview it.
Preview
Theorem 3.2
Blueprint label
  • Frey_curve_hardly_ramified
Group
  • Reducibility of p -torsion of the Frey curve.
✓L∃∀N
Used by 5
Hover a use site to preview it.
Preview
Theorem 3.2
Blueprint label
  • Frey_curve_hardly_ramified
Uses target in
  • statement

Let R be a coefficient ring with finite residue field of characteristic \ell\geq3. Let V be a finite free R-module of rank 2, equipped with the product topology. A continuous representation \rho:\GQ\to \GL_R(V) is said to be hardly ramified if it satisfies the following four conditions:

  • \det(\rho):\GQ\to R^\times is the cyclotomic character.

  • \rho is unramified outside 2\ell.

  • The restriction of \rho to \Gal(\Qbar_2/\Q_2) is reducible. More precisely, there is a short exact sequence 0\to R\to V\to R\to 0 which is stable under the action of \Gal(\Qbar_2/\Q_2), and the Galois action on the 1-dimensional quotient is an unramified representation of \Gal(\Qbar_2/\Q_2) whose square is trivial.

  • The restriction of \rho to \GQl is flat, by which we mean that for all open ideals I of R, the finite-image representation \rho mod I:\GQl\to \GL_{R/I}(V/I) comes from a finite flat group scheme.

Code for Definition3.1●1 definition
  • structure GaloisRepresentation.IsHardlyRamified.{u, u_1} {ℓℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  [FactFact (p : Prop) : PropWrapper for adding elementary propositions to the type class systems.
Warning: this can easily be abused. See the rest of this docstring for details.

Certain propositions should not be treated as a class globally,
but sometimes it is very convenient to be able to use the type class system
in specific circumstances.

For example, `ZMod p` is a field if and only if `p` is a prime number.
In order to be able to find this field instance automatically by type class search,
we have to turn `p.prime` into an instance implicit assumption.

On the other hand, making `Nat.prime` a class would require a major refactoring of the library,
and it is questionable whether making `Nat.prime` a class is desirable at all.
The compromise is to add the assumption `[Fact p.prime]` to `ZMod.field`.

In particular, this class is not intended for turning the type class system
into an automated theorem prover for first-order logic.  (Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  ℓℕ)] (hℓOddOdd ℓ : OddOdd.{u_2} {α : Type u_2} [Semiring α] (a : α) : PropAn element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  ℓℕ) {RType u : Type uA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  RType u]
  [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  RType u] [IsTopologicalRingIsTopologicalRing.{u_1} (R : Type u_1) [TopologicalSpace R] [NonUnitalNonAssocRing R] : PropA topological ring is a ring `R` where addition, multiplication and negation are continuous.

If `R` is a (unital) ring, then continuity of negation can be derived from continuity of
multiplication as it is multiplication with `-1`. (See
`IsTopologicalSemiring.continuousNeg_of_mul` and
`topological_semiring.to_topological_add_group`)  RType u] [IsLocalRingIsLocalRing.{u_1} (R : Type u_1) [Semiring R] : PropA semiring is local if it is nontrivial and `a` or `b` is a unit whenever `a + b = 1`.
Note that `IsLocalRing` is a predicate.  RType u]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. ℓℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u] {VType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  VType u_1] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  RType u VType u_1]
  [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  RType u VType u_1] [Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  RType u VType u_1] (hdimModule.rank R V = 2 : Module.rankModule.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Cardinal.{u_2}The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).


[Stacks Tag 09G3](https://stacks.math.columbia.edu/tag/09G3) (first part) RType u VType u_1 =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 2)
  (ρGaloisRep ℚ R V : GaloisRepGaloisRep.{uK, u_2, u_4} (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`.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 RType u VType u_1) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    structure GaloisRepresentation.IsHardlyRamified.{u,
    u_1}
  {ℓℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} [FactFact (p : Prop) : PropWrapper for adding elementary propositions to the type class systems.
Warning: this can easily be abused. See the rest of this docstring for details.

Certain propositions should not be treated as a class globally,
but sometimes it is very convenient to be able to use the type class system
in specific circumstances.

For example, `ZMod p` is a field if and only if `p` is a prime number.
In order to be able to find this field instance automatically by type class search,
we have to turn `p.prime` into an instance implicit assumption.

On the other hand, making `Nat.prime` a class would require a major refactoring of the library,
and it is questionable whether making `Nat.prime` a class is desirable at all.
The compromise is to add the assumption `[Fact p.prime]` to `ZMod.field`.

In particular, this class is not intended for turning the type class system
into an automated theorem prover for first-order logic.  (Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  ℓℕ)]
  (hℓOddOdd ℓ : OddOdd.{u_2} {α : Type u_2} [Semiring α] (a : α) : PropAn element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  ℓℕ) {RType u : Type uA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  RType u] [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  RType u]
  [IsTopologicalRingIsTopologicalRing.{u_1} (R : Type u_1) [TopologicalSpace R] [NonUnitalNonAssocRing R] : PropA topological ring is a ring `R` where addition, multiplication and negation are continuous.

If `R` is a (unital) ring, then continuity of negation can be derived from continuity of
multiplication as it is multiplication with `-1`. (See
`IsTopologicalSemiring.continuousNeg_of_mul` and
`topological_semiring.to_topological_add_group`)  RType u] [IsLocalRingIsLocalRing.{u_1} (R : Type u_1) [Semiring R] : PropA semiring is local if it is nontrivial and `a` or `b` is a unit whenever `a + b = 1`.
Note that `IsLocalRing` is a predicate.  RType u]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. ℓℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u] {VType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  VType u_1] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  RType u VType u_1]
  [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  RType u VType u_1] [Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  RType u VType u_1]
  (hdimModule.rank R V = 2 : Module.rankModule.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Cardinal.{u_2}The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).


[Stacks Tag 09G3](https://stacks.math.columbia.edu/tag/09G3) (first part) RType u VType u_1 =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 2)
  (ρGaloisRep ℚ R V : GaloisRepGaloisRep.{uK, u_2, u_4} (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`.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 RType u VType u_1) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    Let `R` be a compact Hausdorff local topological ring (for example any complete Noetherian
local ring with the maximal ideal-adic topology) having finite residue field of
characteristic `ℓ > 2`, and let `ρ : Gal(Qbar/Q) → GL_2(R)` be a continuous 2-dimensional
representation. We say that `ρ` is *hardly ramified* if it has cyclotomic determinant, is
unramified outside `2ℓ`, flat at `ℓ` and upper-triangular at 2 with a 1-dimensional quotient which
is unramified and whose square is trivial.

    Constructor

    GaloisRepresentation.IsHardlyRamified.mk.{u,
    u_1}
  {ℓℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} [FactFact (p : Prop) : PropWrapper for adding elementary propositions to the type class systems.
Warning: this can easily be abused. See the rest of this docstring for details.

Certain propositions should not be treated as a class globally,
but sometimes it is very convenient to be able to use the type class system
in specific circumstances.

For example, `ZMod p` is a field if and only if `p` is a prime number.
In order to be able to find this field instance automatically by type class search,
we have to turn `p.prime` into an instance implicit assumption.

On the other hand, making `Nat.prime` a class would require a major refactoring of the library,
and it is questionable whether making `Nat.prime` a class is desirable at all.
The compromise is to add the assumption `[Fact p.prime]` to `ZMod.field`.

In particular, this class is not intended for turning the type class system
into an automated theorem prover for first-order logic.  (Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  ℓℕ)]
  {hℓOddOdd ℓ : OddOdd.{u_2} {α : Type u_2} [Semiring α] (a : α) : PropAn element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  ℓℕ} {RType u : Type uA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  RType u] [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  RType u]
  [IsTopologicalRingIsTopologicalRing.{u_1} (R : Type u_1) [TopologicalSpace R] [NonUnitalNonAssocRing R] : PropA topological ring is a ring `R` where addition, multiplication and negation are continuous.

If `R` is a (unital) ring, then continuity of negation can be derived from continuity of
multiplication as it is multiplication with `-1`. (See
`IsTopologicalSemiring.continuousNeg_of_mul` and
`topological_semiring.to_topological_add_group`)  RType u] [IsLocalRingIsLocalRing.{u_1} (R : Type u_1) [Semiring R] : PropA semiring is local if it is nontrivial and `a` or `b` is a unit whenever `a + b = 1`.
Note that `IsLocalRing` is a predicate.  RType u]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. ℓℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u] {VType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  VType u_1] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  RType u VType u_1]
  [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  RType u VType u_1] [Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  RType u VType u_1]
  {hdimModule.rank R V = 2 : Module.rankModule.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Cardinal.{u_2}The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).


[Stacks Tag 09G3](https://stacks.math.columbia.edu/tag/09G3) (first part) RType u VType u_1 =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 2}
  {ρGaloisRep ℚ R V : GaloisRepGaloisRep.{uK, u_2, u_4} (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`.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 RType u VType u_1}
  (det∀ (g : Field.absoluteGaloisGroup ℚ),
  ρ.det g = (algebraMap ℤ_[ℓ] R) ↑((cyclotomicCharacter (AlgebraicClosure ℚ) ℓ) g.toRingEquiv) :
    ∀ (gField.absoluteGaloisGroup ℚ : Field.absoluteGaloisGroupField.absoluteGaloisGroup.{u_1} (K : Type u_1) [Field K] : Type u_1The absolute Galois group of `K`, defined as the Galois group of the field extension `K^al/K`,
where `K^al` is an algebraic closure of `K`.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
),
      ρGaloisRep ℚ R V.detGaloisRep.det.{uK, u_2, u_4} {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 →ₜ* AThe determinant of a galois rep.  gField.absoluteGaloisGroup ℚ =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
        (algebraMapalgebraMap.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* AEmbedding `R →+* A` given by `Algebra` structure.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. ℓℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u)
          ↑((cyclotomicCharactercyclotomicCharacter.{u} (L : Type u) [CommRing L] [IsDomain L] (p : ℕ) [Fact (Nat.Prime p)] : (L ≃+* L) →* ℤ_[p]ˣSuppose `L` is a domain containing all `pⁱ`-th primitive roots with `p` a (rational) prime.
If `g` is a ring automorphism of `L`, then `cyclotomicCharacter L p g` is the unique `j : ℤₚ` such
that `g(ζ) = ζ ^ (j mod pⁱ)` for all `pⁱ`-th roots of unity `ζ`.

Note: This is the trivial character when `L` does not contain all `pⁱ`-th primitive roots.

                (AlgebraicClosureAlgebraicClosure.{u} (k : Type u) [Field k] : Type uThe canonical algebraic closure of a field, the direct limit of adding roots to the field for
each polynomial over the field.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
) ℓℕ)
              gField.absoluteGaloisGroup ℚ.toRingEquivAlgEquiv.toRingEquiv.{u, v, w} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B]
  [Algebra R A] [Algebra R B] (self : A ≃ₐ[R] B) : A ≃+* B))
  (isUnramified∀ (p : ℕ) (hp : Nat.Prime p), p ≠ 2 ∧ p ≠ ℓ → ρ.IsUnramifiedAt hp.toHeightOneSpectrumRingOfIntegersRat :
    ∀ (pℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) (hpNat.Prime p : Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  pℕ),
      pℕ ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. 2 ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`). pℕ ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. ℓℕ →
        ρGaloisRep ℚ R V.IsUnramifiedAtGaloisRep.IsUnramifiedAt.{uK, u_2, u_4} {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)) : PropThe class of galois reps unramified at `v`. 
          hpNat.Prime p.toHeightOneSpectrumRingOfIntegersRatNat.Prime.toHeightOneSpectrumRingOfIntegersRat {p : ℕ} (hp : Nat.Prime p) :
  IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)The element of `HeightOneSpectrum (𝓞 ℚ)` associated to a prime number. )
  (isFlatGaloisRep.IsFlatAt ⋯.toHeightOneSpectrumRingOfIntegersRat ρ :
    GaloisRep.IsFlatAtGaloisRep.IsFlatAt.{uK, u_2, u_4} {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) : PropA 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`. 
      ⋯.toHeightOneSpectrumRingOfIntegersRatNat.Prime.toHeightOneSpectrumRingOfIntegersRat {p : ℕ} (hp : Nat.Prime p) :
  IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)The element of `HeightOneSpectrum (𝓞 ℚ)` associated to a prime number. 
      ρGaloisRep ℚ R V)
  (isTameAtTwo∃ π,
  ∃ (_ : Function.Surjective ⇑π),
    ∃ δ,
      ∀ (g : Field.absoluteGaloisGroup ℚ_[2]) (v : V),
        π (((ρ.map (algebraMap ℚ ℚ_[2])) g) v) = (δ g) (π v) ∧
          (Submodule.toAddSubgroup (IsLocalRing.maximalIdeal ↥GaloisRepresentation.Z2bar)).inertia
                (Field.absoluteGaloisGroup ℚ_[2]) ≤
              δ.ker ∧
            ∀ (g : Field.absoluteGaloisGroup ℚ_[2]), δ g * δ g = 1 :
    ∃ πV →ₗ[R] R,
      ∃ (_ : Function.SurjectiveFunction.Surjective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : PropA function `f : α → β` is called surjective if every `b : β` is equal to `f a`
for some `a : α`.  ⇑πV →ₗ[R] R),
        ∃ δGaloisRep ℚ_[2] R R,
          ∀
            (gField.absoluteGaloisGroup ℚ_[2] :
              Field.absoluteGaloisGroupField.absoluteGaloisGroup.{u_1} (K : Type u_1) [Field K] : Type u_1The absolute Galois group of `K`, defined as the Galois group of the field extension `K^al/K`,
where `K^al` is an algebraic closure of `K`. 
                ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
2]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
)
            (vV : VType u_1),
            πV →ₗ[R] R
                  (((ρGaloisRep ℚ R V.mapGaloisRep.map.{uK, u_1, u_2, u_4} {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 MA field extension induces a map between galois reps.
Note that this relies on an arbitrarily chosen embedding of the algebraic closures. 
                        (algebraMapalgebraMap.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* AEmbedding `R →+* A` given by `Algebra` structure.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.

                          ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
2]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
))
                      gField.absoluteGaloisGroup ℚ_[2])
                    vV) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
                (δGaloisRep ℚ_[2] R R gField.absoluteGaloisGroup ℚ_[2]) (πV →ₗ[R] R vV) ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
              (Submodule.toAddSubgroupSubmodule.toAddSubgroup.{u, v} {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M}
  (p : Submodule R M) : AddSubgroup MReinterpret a submodule as an additive subgroup. 
                        (IsLocalRing.maximalIdealIsLocalRing.maximalIdeal.{u_1} (R : Type u_1) [CommSemiring R] [IsLocalRing R] : Ideal RThe ideal of elements that are not units. 
                          ↥GaloisRepresentation.Z2barGaloisRepresentation.Z2bar : ValuationSubring (AlgebraicClosure ℚ_[2])Z2bar is the ring of integers of `ℚ_[2]ᵃˡᵍ`. )).inertiaAddSubgroup.inertia.{u_6, u_7} {M : Type u_6} [AddGroup M] (I : AddSubgroup M) (G : Type u_7) [Group G]
  [MulAction G M] : Subgroup GSuppose `G` acts on `M` and `I` is a subgroup of `M`.
The inertia subgroup of `I` is the subgroup of `G` whose action is trivial mod `I`. 
                    (Field.absoluteGaloisGroupField.absoluteGaloisGroup.{u_1} (K : Type u_1) [Field K] : Type u_1The absolute Galois group of `K`, defined as the Galois group of the field extension `K^al/K`,
where `K^al` is an algebraic closure of `K`. 
                      ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
2]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
) ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`).
                  δGaloisRep ℚ_[2] R R.kerGaloisRep.ker.{uK, u_2, u_4} {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.  ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
                ∀
                  (gField.absoluteGaloisGroup ℚ_[2] :
                    Field.absoluteGaloisGroupField.absoluteGaloisGroup.{u_1} (K : Type u_1) [Field K] : Type u_1The absolute Galois group of `K`, defined as the Galois group of the field extension `K^al/K`,
where `K^al` is an algebraic closure of `K`. 
                      ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
2]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
),
                  δGaloisRep ℚ_[2] R R gField.absoluteGaloisGroup ℚ_[2] *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. δGaloisRep ℚ_[2] R R gField.absoluteGaloisGroup ℚ_[2] =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1) :
  GaloisRepresentation.IsHardlyRamifiedGaloisRepresentation.IsHardlyRamified.{u, u_1} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓOdd : Odd ℓ) {R : Type u} [CommRing R]
  [TopologicalSpace R] [IsTopologicalRing R] [IsLocalRing R] [Algebra ℤ_[ℓ] R] {V : Type u_1} [AddCommGroup V]
  [Module R V] [Module.Finite R V] [Module.Free R V] (hdim : Module.rank R V = 2) (ρ : GaloisRep ℚ R V) : PropLet `R` be a compact Hausdorff local topological ring (for example any complete Noetherian
local ring with the maximal ideal-adic topology) having finite residue field of
characteristic `ℓ > 2`, and let `ρ : Gal(Qbar/Q) → GL_2(R)` be a continuous 2-dimensional
representation. We say that `ρ` is *hardly ramified* if it has cyclotomic determinant, is
unramified outside `2ℓ`, flat at `ℓ` and upper-triangular at 2 with a 1-dimensional quotient which
is unramified and whose square is trivial. 
    hℓOddOdd ℓ hdimModule.rank R V = 2 ρGaloisRep ℚ R V

    Fields

    det∀ (g : Field.absoluteGaloisGroup ℚ),
  ρ.det g = (algebraMap ℤ_[ℓ] R) ↑((cyclotomicCharacter (AlgebraicClosure ℚ) ℓ) g.toRingEquiv) : ∀ (gField.absoluteGaloisGroup ℚ : Field.absoluteGaloisGroupField.absoluteGaloisGroup.{u_1} (K : Type u_1) [Field K] : Type u_1The absolute Galois group of `K`, defined as the Galois group of the field extension `K^al/K`,
where `K^al` is an algebraic closure of `K`.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
),
  ρGaloisRep ℚ R V.detGaloisRep.det.{uK, u_2, u_4} {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 →ₜ* AThe determinant of a galois rep.  gField.absoluteGaloisGroup ℚ =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. (algebraMapalgebraMap.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* AEmbedding `R →+* A` given by `Algebra` structure.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. ℓℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u) ↑((cyclotomicCharactercyclotomicCharacter.{u} (L : Type u) [CommRing L] [IsDomain L] (p : ℕ) [Fact (Nat.Prime p)] : (L ≃+* L) →* ℤ_[p]ˣSuppose `L` is a domain containing all `pⁱ`-th primitive roots with `p` a (rational) prime.
If `g` is a ring automorphism of `L`, then `cyclotomicCharacter L p g` is the unique `j : ℤₚ` such
that `g(ζ) = ζ ^ (j mod pⁱ)` for all `pⁱ`-th roots of unity `ζ`.

Note: This is the trivial character when `L` does not contain all `pⁱ`-th primitive roots.
 (AlgebraicClosureAlgebraicClosure.{u} (k : Type u) [Field k] : Type uThe canonical algebraic closure of a field, the direct limit of adding roots to the field for
each polynomial over the field.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
) ℓℕ) gField.absoluteGaloisGroup ℚ.toRingEquivAlgEquiv.toRingEquiv.{u, v, w} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B]
  [Algebra R A] [Algebra R B] (self : A ≃ₐ[R] B) : A ≃+* B)
    isUnramified∀ (p : ℕ) (hp : Nat.Prime p), p ≠ 2 ∧ p ≠ ℓ → ρ.IsUnramifiedAt hp.toHeightOneSpectrumRingOfIntegersRat : ∀ (pℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) (hpNat.Prime p : Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  pℕ), pℕ ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. 2 ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`). pℕ ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. ℓℕ → ρGaloisRep ℚ R V.IsUnramifiedAtGaloisRep.IsUnramifiedAt.{uK, u_2, u_4} {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)) : PropThe class of galois reps unramified at `v`.  hpNat.Prime p.toHeightOneSpectrumRingOfIntegersRatNat.Prime.toHeightOneSpectrumRingOfIntegersRat {p : ℕ} (hp : Nat.Prime p) :
  IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)The element of `HeightOneSpectrum (𝓞 ℚ)` associated to a prime number. 
    isFlatGaloisRep.IsFlatAt ⋯.toHeightOneSpectrumRingOfIntegersRat ρ : GaloisRep.IsFlatAtGaloisRep.IsFlatAt.{uK, u_2, u_4} {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) : PropA 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`.  ⋯.toHeightOneSpectrumRingOfIntegersRatNat.Prime.toHeightOneSpectrumRingOfIntegersRat {p : ℕ} (hp : Nat.Prime p) :
  IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)The element of `HeightOneSpectrum (𝓞 ℚ)` associated to a prime number.  ρGaloisRep ℚ R V
    isTameAtTwo∃ π,
  ∃ (_ : Function.Surjective ⇑π),
    ∃ δ,
      ∀ (g : Field.absoluteGaloisGroup ℚ_[2]) (v : V),
        π (((ρ.map (algebraMap ℚ ℚ_[2])) g) v) = (δ g) (π v) ∧
          (Submodule.toAddSubgroup (IsLocalRing.maximalIdeal ↥GaloisRepresentation.Z2bar)).inertia
                (Field.absoluteGaloisGroup ℚ_[2]) ≤
              δ.ker ∧
            ∀ (g : Field.absoluteGaloisGroup ℚ_[2]), δ g * δ g = 1 : ∃ πV →ₗ[R] R,
  ∃ (_ : Function.SurjectiveFunction.Surjective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : PropA function `f : α → β` is called surjective if every `b : β` is equal to `f a`
for some `a : α`.  ⇑πV →ₗ[R] R),
    ∃ δGaloisRep ℚ_[2] R R,
      ∀ (gField.absoluteGaloisGroup ℚ_[2] : Field.absoluteGaloisGroupField.absoluteGaloisGroup.{u_1} (K : Type u_1) [Field K] : Type u_1The absolute Galois group of `K`, defined as the Galois group of the field extension `K^al/K`,
where `K^al` is an algebraic closure of `K`.  ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
2]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
) (vV : VType u_1),
        πV →ₗ[R] R (((ρGaloisRep ℚ R V.mapGaloisRep.map.{uK, u_1, u_2, u_4} {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 MA field extension induces a map between galois reps.
Note that this relies on an arbitrarily chosen embedding of the algebraic closures.  (algebraMapalgebraMap.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* AEmbedding `R →+* A` given by `Algebra` structure.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
2]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
)) gField.absoluteGaloisGroup ℚ_[2]) vV) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. (δGaloisRep ℚ_[2] R R gField.absoluteGaloisGroup ℚ_[2]) (πV →ₗ[R] R vV) ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
          (Submodule.toAddSubgroupSubmodule.toAddSubgroup.{u, v} {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M}
  (p : Submodule R M) : AddSubgroup MReinterpret a submodule as an additive subgroup.  (IsLocalRing.maximalIdealIsLocalRing.maximalIdeal.{u_1} (R : Type u_1) [CommSemiring R] [IsLocalRing R] : Ideal RThe ideal of elements that are not units.  ↥GaloisRepresentation.Z2barGaloisRepresentation.Z2bar : ValuationSubring (AlgebraicClosure ℚ_[2])Z2bar is the ring of integers of `ℚ_[2]ᵃˡᵍ`. )).inertiaAddSubgroup.inertia.{u_6, u_7} {M : Type u_6} [AddGroup M] (I : AddSubgroup M) (G : Type u_7) [Group G]
  [MulAction G M] : Subgroup GSuppose `G` acts on `M` and `I` is a subgroup of `M`.
The inertia subgroup of `I` is the subgroup of `G` whose action is trivial mod `I`. 
                (Field.absoluteGaloisGroupField.absoluteGaloisGroup.{u_1} (K : Type u_1) [Field K] : Type u_1The absolute Galois group of `K`, defined as the Galois group of the field extension `K^al/K`,
where `K^al` is an algebraic closure of `K`.  ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
2]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
) ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`).
              δGaloisRep ℚ_[2] R R.kerGaloisRep.ker.{uK, u_2, u_4} {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.  ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
            ∀ (gField.absoluteGaloisGroup ℚ_[2] : Field.absoluteGaloisGroupField.absoluteGaloisGroup.{u_1} (K : Type u_1) [Field K] : Type u_1The absolute Galois group of `K`, defined as the Galois group of the field extension `K^al/K`,
where `K^al` is an algebraic closure of `K`.  ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
2]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
), δGaloisRep ℚ_[2] R R gField.absoluteGaloisGroup ℚ_[2] *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. δGaloisRep ℚ_[2] R R gField.absoluteGaloisGroup ℚ_[2] =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1
    complete

A well-known result, which basically goes back to Frey, is the following:

Theorem3.2
Group: Reducibility of p -torsion of the Frey curve. (7)
Hover another entry in this group to preview it.
Preview
Definition 3.1
Blueprint label
  • hardly_ramified
Group
  • Reducibility of p -torsion of the Frey curve.
⚠L∃∀N
Used by 2
Hover a use site to preview it.
Preview
Theorem 2.8
Blueprint label
  • Wiles_Frey
Uses target in
  • proof

Definition 3.1 The \ell-torsion representation in the Frey curve attached to a Frey package (a,b,c,\ell) is hardly ramified.

Code for Theorem3.2●1 theorem, incomplete
  • theorem FreyCurve.torsion_isHardlyRamified (PFreyPackage : FreyPackageFreyPackage : TypeA *Frey Package* is a 4-tuple (a,b,c,p) of integers
satisfying $a^p+b^p=c^p$ and some other inequalities
and congruences. These facts guarantee that all of
the all the results in section 4.1 of Serre's paper [serre]
apply to the curve $Y^2=X(X-a^p)(X+b^p).$
) :
  GaloisRepresentation.IsHardlyRamifiedGaloisRepresentation.IsHardlyRamified.{u, u_1} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓOdd : Odd ℓ) {R : Type u} [CommRing R]
  [TopologicalSpace R] [IsTopologicalRing R] [IsLocalRing R] [Algebra ℤ_[ℓ] R] {V : Type u_1} [AddCommGroup V]
  [Module R V] [Module.Finite R V] [Module.Free R V] (hdim : Module.rank R V = 2) (ρ : GaloisRep ℚ R V) : PropLet `R` be a compact Hausdorff local topological ring (for example any complete Noetherian
local ring with the maximal ideal-adic topology) having finite residue field of
characteristic `ℓ > 2`, and let `ρ : Gal(Qbar/Q) → GL_2(R)` be a continuous 2-dimensional
representation. We say that `ρ` is *hardly ramified* if it has cyclotomic determinant, is
unramified outside `2ℓ`, flat at `ℓ` and upper-triangular at 2 with a 1-dimensional quotient which
is unramified and whose square is trivial.  ⋯ ⋯
    (PFreyPackage.freyCurveFreyPackage.freyCurve (P : FreyPackage) : WeierstrassCurve ℚThe elliptic curve over `ℚ` associated to a Frey package. The conditions imposed
upon a Frey package guarantee that the running hypotheses in
Section 4.1 of [Serre] all hold. We put the curve into the form where the
equation is semistable at 2, rather than the usual `Y^2=X(X-a^p)(X+b^p)` form.
The change of variables is `X=4x` and `Y=8y+4x`, and then divide through by 64. .galoisRepWeierstrassCurve.galoisRep.{u} {K : Type u} [Field K] (E : WeierstrassCurve K) [E.IsElliptic] [DecidableEq K]
  [DecidableEq (AlgebraicClosure K)] (n : ℕ) (hn : 0 < n) :
  GaloisRep K (ZMod n) ((E.map (algebraMap K (AlgebraicClosure K))).n_torsion n)The continuous Galois representation associated to an elliptic curve over a field.  PFreyPackage.pFreyPackage.p (self : FreyPackage) : ℕThe prime number `p` in the Frey package.  ⋯)
    theorem FreyCurve.torsion_isHardlyRamified
  (PFreyPackage : FreyPackageFreyPackage : TypeA *Frey Package* is a 4-tuple (a,b,c,p) of integers
satisfying $a^p+b^p=c^p$ and some other inequalities
and congruences. These facts guarantee that all of
the all the results in section 4.1 of Serre's paper [serre]
apply to the curve $Y^2=X(X-a^p)(X+b^p).$
) :
  GaloisRepresentation.IsHardlyRamifiedGaloisRepresentation.IsHardlyRamified.{u, u_1} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓOdd : Odd ℓ) {R : Type u} [CommRing R]
  [TopologicalSpace R] [IsTopologicalRing R] [IsLocalRing R] [Algebra ℤ_[ℓ] R] {V : Type u_1} [AddCommGroup V]
  [Module R V] [Module.Finite R V] [Module.Free R V] (hdim : Module.rank R V = 2) (ρ : GaloisRep ℚ R V) : PropLet `R` be a compact Hausdorff local topological ring (for example any complete Noetherian
local ring with the maximal ideal-adic topology) having finite residue field of
characteristic `ℓ > 2`, and let `ρ : Gal(Qbar/Q) → GL_2(R)` be a continuous 2-dimensional
representation. We say that `ρ` is *hardly ramified* if it has cyclotomic determinant, is
unramified outside `2ℓ`, flat at `ℓ` and upper-triangular at 2 with a 1-dimensional quotient which
is unramified and whose square is trivial.  ⋯
    ⋯ (PFreyPackage.freyCurveFreyPackage.freyCurve (P : FreyPackage) : WeierstrassCurve ℚThe elliptic curve over `ℚ` associated to a Frey package. The conditions imposed
upon a Frey package guarantee that the running hypotheses in
Section 4.1 of [Serre] all hold. We put the curve into the form where the
equation is semistable at 2, rather than the usual `Y^2=X(X-a^p)(X+b^p)` form.
The change of variables is `X=4x` and `Y=8y+4x`, and then divide through by 64. .galoisRepWeierstrassCurve.galoisRep.{u} {K : Type u} [Field K] (E : WeierstrassCurve K) [E.IsElliptic] [DecidableEq K]
  [DecidableEq (AlgebraicClosure K)] (n : ℕ) (hn : 0 < n) :
  GaloisRep K (ZMod n) ((E.map (algebraMap K (AlgebraicClosure K))).n_torsion n)The continuous Galois representation associated to an elliptic curve over a field.  PFreyPackage.pFreyPackage.p (self : FreyPackage) : ℕThe prime number `p` in the Frey package.  ⋯)
    contains sorry in statement
Proof

This was well-known in the 1980s. A proof sketch is as follows. First note that \ell \ge 5 > 3 by definition of a Frey package. Let \rho denote the Galois representation on the \ell-torsion of the Frey curve. The fact that \rho is 2-dimensional is Corollary~III.6.4(b) of (Silverman, 2009), and the fact that its determinant is cyclotomic is Proposition~III.8.3 of the same reference. These results hold for elliptic curves in general. The remaining claims are specific to the Frey curve and lie deeper. The fact that \rho is unramified outside 2\ell is a consequence of (4.1.12) and (4.1.13) of (Serre, 1987). The fact that \rho at 2 has an unramified 1-dimensional quotient of order at most 2 follows from the fact that the Frey curve is semistable at 2 and the theory of the Tate curve. Finally, the claim that \rho is flat at \ell is Proposition~5 and (4.1.13) of (Serre, 1987).

Note that irreducibility and absolute irreducibility for hardly ramified mod \ell representations are the same, because our assumptions that \ell\geq3 and that the determinant is cyclotomic imply that the image of complex conjugation has distinct eigenvalues defined over the ground field.

Theorem3.3
Group: Reducibility of p -torsion of the Frey curve. (7)
Hover another entry in this group to preview it.
Preview
Definition 3.1
Blueprint label
  • hardly_ramified
Group
  • Reducibility of p -torsion of the Frey curve.
⚠L∃∀N
Used by 2
Hover a use site to preview it.
Preview
Theorem 2.8
Blueprint label
  • Wiles_Frey
Uses target in
  • proof

If \ell \ge 3 is prime and \rho : \GQ \to \GL_2(\mathbf{Z}/\ell\mathbf{Z}) is hardly ramified, then \rho is reducible.

Code for Theorem3.3●1 theorem, incomplete
  • theorem FreyCurve.torsion_not_isIrreducible (PFreyPackage : FreyPackageFreyPackage : TypeA *Frey Package* is a 4-tuple (a,b,c,p) of integers
satisfying $a^p+b^p=c^p$ and some other inequalities
and congruences. These facts guarantee that all of
the all the results in section 4.1 of Serre's paper [serre]
apply to the curve $Y^2=X(X-a^p)(X+b^p).$
) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.(PFreyPackage.freyCurveFreyPackage.freyCurve (P : FreyPackage) : WeierstrassCurve ℚThe elliptic curve over `ℚ` associated to a Frey package. The conditions imposed
upon a Frey package guarantee that the running hypotheses in
Section 4.1 of [Serre] all hold. We put the curve into the form where the
equation is semistable at 2, rather than the usual `Y^2=X(X-a^p)(X+b^p)` form.
The change of variables is `X=4x` and `Y=8y+4x`, and then divide through by 64. .galoisRepWeierstrassCurve.galoisRep.{u} {K : Type u} [Field K] (E : WeierstrassCurve K) [E.IsElliptic] [DecidableEq K]
  [DecidableEq (AlgebraicClosure K)] (n : ℕ) (hn : 0 < n) :
  GaloisRep K (ZMod n) ((E.map (algebraMap K (AlgebraicClosure K))).n_torsion n)The continuous Galois representation associated to an elliptic curve over a field.  PFreyPackage.pFreyPackage.p (self : FreyPackage) : ℕThe prime number `p` in the Frey package.  ⋯).IsIrreducibleGaloisRep.IsIrreducible.{uK, u_4, u_7} {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) : PropIrreducibility of a Galois representation over a field. 
    theorem FreyCurve.torsion_not_isIrreducible
  (PFreyPackage : FreyPackageFreyPackage : TypeA *Frey Package* is a 4-tuple (a,b,c,p) of integers
satisfying $a^p+b^p=c^p$ and some other inequalities
and congruences. These facts guarantee that all of
the all the results in section 4.1 of Serre's paper [serre]
apply to the curve $Y^2=X(X-a^p)(X+b^p).$
) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.(PFreyPackage.freyCurveFreyPackage.freyCurve (P : FreyPackage) : WeierstrassCurve ℚThe elliptic curve over `ℚ` associated to a Frey package. The conditions imposed
upon a Frey package guarantee that the running hypotheses in
Section 4.1 of [Serre] all hold. We put the curve into the form where the
equation is semistable at 2, rather than the usual `Y^2=X(X-a^p)(X+b^p)` form.
The change of variables is `X=4x` and `Y=8y+4x`, and then divide through by 64. .galoisRepWeierstrassCurve.galoisRep.{u} {K : Type u} [Field K] (E : WeierstrassCurve K) [E.IsElliptic] [DecidableEq K]
  [DecidableEq (AlgebraicClosure K)] (n : ℕ) (hn : 0 < n) :
  GaloisRep K (ZMod n) ((E.map (algebraMap K (AlgebraicClosure K))).n_torsion n)The continuous Galois representation associated to an elliptic curve over a field.  PFreyPackage.pFreyPackage.p (self : FreyPackage) : ℕThe prime number `p` in the Frey package. 
        ⋯).IsIrreducibleGaloisRep.IsIrreducible.{uK, u_4, u_7} {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) : PropIrreducibility of a Galois representation over a field.
    contains sorry in proof

Note that this (deep) claim is a consequence of Serre's conjecture (Serre, 1987), now a theorem of Khare and Wintenberger (Khare and Wintenberger, 2009), and indeed we shall use methods introduced by Khare and Wintenberger to prove this special case of Serre's conjecture. Given this result, we can deduce theorem Wiles_Frey (which we restate here) easily:

Theorem3.4
Group: Reducibility of p -torsion of the Frey curve. (7)
Hover another entry in this group to preview it.
Preview
Definition 3.1
Blueprint label
  • hardly_ramified
Group
  • Reducibility of p -torsion of the Frey curve.
✓L∃∀Nused by 0

If \overline{\rho} is the mod p Galois representation associated to a Frey package (a,b,c,p) then \overline{\rho} is reducible.

Code for Theorem3.4●1 theorem
  • theorem Wiles_Frey (PFreyPackage : FreyPackageFreyPackage : TypeA *Frey Package* is a 4-tuple (a,b,c,p) of integers
satisfying $a^p+b^p=c^p$ and some other inequalities
and congruences. These facts guarantee that all of
the all the results in section 4.1 of Serre's paper [serre]
apply to the curve $Y^2=X(X-a^p)(X+b^p).$
) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.(PFreyPackage.freyCurveFreyPackage.freyCurve (P : FreyPackage) : WeierstrassCurve ℚThe elliptic curve over `ℚ` associated to a Frey package. The conditions imposed
upon a Frey package guarantee that the running hypotheses in
Section 4.1 of [Serre] all hold. We put the curve into the form where the
equation is semistable at 2, rather than the usual `Y^2=X(X-a^p)(X+b^p)` form.
The change of variables is `X=4x` and `Y=8y+4x`, and then divide through by 64. .galoisRepWeierstrassCurve.galoisRep.{u} {K : Type u} [Field K] (E : WeierstrassCurve K) [E.IsElliptic] [DecidableEq K]
  [DecidableEq (AlgebraicClosure K)] (n : ℕ) (hn : 0 < n) :
  GaloisRep K (ZMod n) ((E.map (algebraMap K (AlgebraicClosure K))).n_torsion n)The continuous Galois representation associated to an elliptic curve over a field.  PFreyPackage.pFreyPackage.p (self : FreyPackage) : ℕThe prime number `p` in the Frey package.  ⋯).IsIrreducibleGaloisRep.IsIrreducible.{uK, u_4, u_7} {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) : PropIrreducibility of a Galois representation over a field. 
    theorem Wiles_Frey (PFreyPackage : FreyPackageFreyPackage : TypeA *Frey Package* is a 4-tuple (a,b,c,p) of integers
satisfying $a^p+b^p=c^p$ and some other inequalities
and congruences. These facts guarantee that all of
the all the results in section 4.1 of Serre's paper [serre]
apply to the curve $Y^2=X(X-a^p)(X+b^p).$
) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.(PFreyPackage.freyCurveFreyPackage.freyCurve (P : FreyPackage) : WeierstrassCurve ℚThe elliptic curve over `ℚ` associated to a Frey package. The conditions imposed
upon a Frey package guarantee that the running hypotheses in
Section 4.1 of [Serre] all hold. We put the curve into the form where the
equation is semistable at 2, rather than the usual `Y^2=X(X-a^p)(X+b^p)` form.
The change of variables is `X=4x` and `Y=8y+4x`, and then divide through by 64. .galoisRepWeierstrassCurve.galoisRep.{u} {K : Type u} [Field K] (E : WeierstrassCurve K) [E.IsElliptic] [DecidableEq K]
  [DecidableEq (AlgebraicClosure K)] (n : ℕ) (hn : 0 < n) :
  GaloisRep K (ZMod n) ((E.map (algebraMap K (AlgebraicClosure K))).n_torsion n)The continuous Galois representation associated to an elliptic curve over a field.  PFreyPackage.pFreyPackage.p (self : FreyPackage) : ℕThe prime number `p` in the Frey package. 
        ⋯).IsIrreducibleGaloisRep.IsIrreducible.{uK, u_4, u_7} {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) : PropIrreducibility of a Galois representation over a field.
    complete
Proof

Theorem 3.2 Theorem 3.3 Indeed, \rho is hardly ramified by the former theorem and thus reducible by the latter.

Our job of reducing FLT to theorems of the 1980s is hence reduced to proving hardly_ramified_reducible.

3.2.1. Hardly Ramified Mod p Representations Are Reducible🔗

In this section we will state three theorems, from which hardly_ramified_reducible easily follows.

Firstly, we claim that an irreducible hardly ramified mod \ell representation lifts to an \ell-adic representation.

Theorem3.5
Group: Reducibility of p -torsion of the Frey curve. (7)
Hover another entry in this group to preview it.
Preview
Definition 3.1
Blueprint label
  • hardly_ramified
Group
  • Reducibility of p -torsion of the Frey curve.
⚠L∃∀Nused by 1

Definition 3.1 If \ell \ge 3 is prime and \overline{\rho} : \GQ \to \GL_2(\mathbf{Z}/\ell\mathbf{Z}) is hardly ramified and irreducible, then there exists a finite extension K / \Q_\ell with integer ring \mathcal{O} and maximal ideal \mathfrak{m} and a hardly ramified representation \rho : \GQ \to \GL_2(\mathcal{O}) whose reduction modulo \mathfrak{m} is isomorphic to \overline{\rho}.

Code for Theorem3.5●1 theorem, incomplete
  • theorem GaloisRepresentation.IsHardlyRamified.lifts.{u, v} {kType u : Type uA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 kType u] [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  kType u] [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  kType u] [DiscreteTopologyDiscreteTopology.{u_2} (α : Type u_2) [t : TopologicalSpace α] : PropA topological space is discrete if every set is open, that is,
its topology equals the discrete topology `⊥`.  kType u] {pℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  (hpoddOdd p : OddOdd.{u_2} {α : Type u_2} [Semiring α] (a : α) : PropAn element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  pℕ) [FactFact (p : Prop) : PropWrapper for adding elementary propositions to the type class systems.
Warning: this can easily be abused. See the rest of this docstring for details.

Certain propositions should not be treated as a class globally,
but sometimes it is very convenient to be able to use the type class system
in specific circumstances.

For example, `ZMod p` is a field if and only if `p` is a prime number.
In order to be able to find this field instance automatically by type class search,
we have to turn `p.prime` into an instance implicit assumption.

On the other hand, making `Nat.prime` a class would require a major refactoring of the library,
and it is questionable whether making `Nat.prime` a class is desirable at all.
The compromise is to add the assumption `[Fact p.prime]` to `ZMod.field`.

In particular, this class is not intended for turning the type class system
into an automated theorem prover for first-order logic.  (Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  pℕ)] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  kType u]
  [IsLocalHomIsLocalHom.{u_2, u_3, u_5} {R : Type u_2} {S : Type u_3} {F : Type u_5} [Monoid R] [Monoid S] [FunLike F R S] (f : F) :
  PropA map `f` between monoids is *local* if any `a` in the domain is a unit
whenever `f a` is a unit. See `IsLocalRing.local_hom_TFAE` for other equivalent
definitions in the local ring case - from where this concept originates, but it is useful in
other contexts, so we allow this generalisation in mathlib.  (algebraMapalgebraMap.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* AEmbedding `R →+* A` given by `Algebra` structure.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  kType u)] (VType v : Type vA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  VType v]
  [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  kType u VType v] [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  kType u VType v] [Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  kType u VType v]
  (hVModule.rank k V = 2 : Module.rankModule.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Cardinal.{u_2}The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).


[Stacks Tag 09G3](https://stacks.math.columbia.edu/tag/09G3) (first part) kType u VType v =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 2) (ρGaloisRep ℚ k V : GaloisRepGaloisRep.{uK, u_2, u_4} (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`.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 kType u VType v)
  (hρirredρ.IsIrreducible : ρGaloisRep ℚ k V.IsIrreducibleGaloisRep.IsIrreducible.{uK, u_4, u_7} {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) : PropIrreducibility of a Galois representation over a field. )
  (hρGaloisRepresentation.IsHardlyRamified hpodd hV ρ : GaloisRepresentation.IsHardlyRamifiedGaloisRepresentation.IsHardlyRamified.{u, u_1} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓOdd : Odd ℓ) {R : Type u} [CommRing R]
  [TopologicalSpace R] [IsTopologicalRing R] [IsLocalRing R] [Algebra ℤ_[ℓ] R] {V : Type u_1} [AddCommGroup V]
  [Module R V] [Module.Finite R V] [Module.Free R V] (hdim : Module.rank R V = 2) (ρ : GaloisRep ℚ R V) : PropLet `R` be a compact Hausdorff local topological ring (for example any complete Noetherian
local ring with the maximal ideal-adic topology) having finite residue field of
characteristic `ℓ > 2`, and let `ρ : Gal(Qbar/Q) → GL_2(R)` be a continuous 2-dimensional
representation. We say that `ρ` is *hardly ramified* if it has cyclotomic determinant, is
unramified outside `2ℓ`, flat at `ℓ` and upper-triangular at 2 with a 1-dimensional quotient which
is unramified and whose square is trivial.  hpoddOdd p hVModule.rank k V = 2 ρGaloisRep ℚ k V) :
  ∃ RType u xCommRing R,
    ∃ (x_1IsLocalRing R : IsLocalRingIsLocalRing.{u_1} (R : Type u_1) [Semiring R] : PropA semiring is local if it is nontrivial and `a` or `b` is a unit whenever `a + b = 1`.
Note that `IsLocalRing` is a predicate.  RType u),
      ∃ x_2TopologicalSpace R,
        ∃ (x_3IsTopologicalRing R : IsTopologicalRingIsTopologicalRing.{u_1} (R : Type u_1) [TopologicalSpace R] [NonUnitalNonAssocRing R] : PropA topological ring is a ring `R` where addition, multiplication and negation are continuous.

If `R` is a (unital) ring, then continuity of negation can be derived from continuity of
multiplication as it is multiplication with `-1`. (See
`IsTopologicalSemiring.continuousNeg_of_mul` and
`topological_semiring.to_topological_add_group`)  RType u),
          ∃ x_4Algebra ℤ_[p] R,
            ∃ (_ : IsLocalHomIsLocalHom.{u_2, u_3, u_5} {R : Type u_2} {S : Type u_3} {F : Type u_5} [Monoid R] [Monoid S] [FunLike F R S] (f : F) :
  PropA map `f` between monoids is *local* if any `a` in the domain is a unit
whenever `f a` is a unit. See `IsLocalRing.local_hom_TFAE` for other equivalent
definitions in the local ring case - from where this concept originates, but it is useful in
other contexts, so we allow this generalisation in mathlib.  (algebraMapalgebraMap.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* AEmbedding `R →+* A` given by `Algebra` structure.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u)) (_ :
              Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u) (_ : Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u) (_ :
              IsModuleTopologyIsModuleTopology.{u_1, u_2} (R : Type u_1) [TopologicalSpace R] (A : Type u_2) [Add A] [SMul R A]
  [τA : TopologicalSpace A] : PropA class asserting that the topology on a module over a topological ring `R` is
the module topology. See `moduleTopology` for more discussion of the module topology.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u),
              ∃ x_9Algebra R k,
                ∃ (_ : IsScalarTowerIsScalarTower.{u_9, u_10, u_11} (M : Type u_9) (N : Type u_10) (α : Type u_11) [SMul M N] [SMul N α] [SMul M α] : PropAn instance of `IsScalarTower M N α` states that the multiplicative
action of `M` on `α` is determined by the multiplicative actions of `M` on `N`
and `N` on `α`.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u kType u) (x_11ContinuousSMul R k :
                  ContinuousSMulContinuousSMul.{u_1, u_2} (M : Type u_1) (X : Type u_2) [SMul M X] [TopologicalSpace M] [TopologicalSpace X] : PropClass `ContinuousSMul M X` says that the scalar multiplication `(•) : M → X → X`
is continuous in both arguments. We use the same class for all kinds of multiplicative actions,
including (semi)modules and algebras.  RType u kType u),
                  ∃ WType v x_12AddCommGroup W x_13Module R W,
                    ∃ (x_14Module.Finite R W : Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  RType u WType v) (x_15Module.Free R W :
                      Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  RType u WType v) (hWModule.rank R W = 2 : Module.rankModule.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Cardinal.{u_2}The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).


[Stacks Tag 09G3](https://stacks.math.columbia.edu/tag/09G3) (first part) RType u WType v =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 2),
                      ∃ σGaloisRep ℚ R W rTensorProduct R k W ≃ₗ[k] V,
                        GaloisRepresentation.IsHardlyRamifiedGaloisRepresentation.IsHardlyRamified.{u, u_1} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓOdd : Odd ℓ) {R : Type u} [CommRing R]
  [TopologicalSpace R] [IsTopologicalRing R] [IsLocalRing R] [Algebra ℤ_[ℓ] R] {V : Type u_1} [AddCommGroup V]
  [Module R V] [Module.Finite R V] [Module.Free R V] (hdim : Module.rank R V = 2) (ρ : GaloisRep ℚ R V) : PropLet `R` be a compact Hausdorff local topological ring (for example any complete Noetherian
local ring with the maximal ideal-adic topology) having finite residue field of
characteristic `ℓ > 2`, and let `ρ : Gal(Qbar/Q) → GL_2(R)` be a continuous 2-dimensional
representation. We say that `ρ` is *hardly ramified* if it has cyclotomic determinant, is
unramified outside `2ℓ`, flat at `ℓ` and upper-triangular at 2 with a 1-dimensional quotient which
is unramified and whose square is trivial.  hpoddOdd p hWModule.rank R W = 2
                            σGaloisRep ℚ R W ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
                          (GaloisRep.baseChangeGaloisRep.baseChange.{uK, u_2, u_3, u_4} {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`.  kType u σGaloisRep ℚ R W).conjGaloisRep.conj.{uK, u_2, u_4, u_5} {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 NWe can conjugate a galois rep by a linear isomorphism on the space.  rTensorProduct R k W ≃ₗ[k] V =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. ρGaloisRep ℚ k V
    theorem GaloisRepresentation.IsHardlyRamified.lifts.{u,
    v}
  {kType u : Type uA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 kType u] [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  kType u]
  [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  kType u]
  [DiscreteTopologyDiscreteTopology.{u_2} (α : Type u_2) [t : TopologicalSpace α] : PropA topological space is discrete if every set is open, that is,
its topology equals the discrete topology `⊥`.  kType u] {pℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  (hpoddOdd p : OddOdd.{u_2} {α : Type u_2} [Semiring α] (a : α) : PropAn element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  pℕ) [FactFact (p : Prop) : PropWrapper for adding elementary propositions to the type class systems.
Warning: this can easily be abused. See the rest of this docstring for details.

Certain propositions should not be treated as a class globally,
but sometimes it is very convenient to be able to use the type class system
in specific circumstances.

For example, `ZMod p` is a field if and only if `p` is a prime number.
In order to be able to find this field instance automatically by type class search,
we have to turn `p.prime` into an instance implicit assumption.

On the other hand, making `Nat.prime` a class would require a major refactoring of the library,
and it is questionable whether making `Nat.prime` a class is desirable at all.
The compromise is to add the assumption `[Fact p.prime]` to `ZMod.field`.

In particular, this class is not intended for turning the type class system
into an automated theorem prover for first-order logic.  (Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  pℕ)]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  kType u]
  [IsLocalHomIsLocalHom.{u_2, u_3, u_5} {R : Type u_2} {S : Type u_3} {F : Type u_5} [Monoid R] [Monoid S] [FunLike F R S] (f : F) :
  PropA map `f` between monoids is *local* if any `a` in the domain is a unit
whenever `f a` is a unit. See `IsLocalRing.local_hom_TFAE` for other equivalent
definitions in the local ring case - from where this concept originates, but it is useful in
other contexts, so we allow this generalisation in mathlib.  (algebraMapalgebraMap.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* AEmbedding `R →+* A` given by `Algebra` structure.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  kType u)]
  (VType v : Type vA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  VType v]
  [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  kType u VType v] [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  kType u VType v]
  [Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  kType u VType v]
  (hVModule.rank k V = 2 : Module.rankModule.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Cardinal.{u_2}The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).


[Stacks Tag 09G3](https://stacks.math.columbia.edu/tag/09G3) (first part) kType u VType v =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 2)
  (ρGaloisRep ℚ k V : GaloisRepGaloisRep.{uK, u_2, u_4} (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`.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 kType u VType v)
  (hρirredρ.IsIrreducible : ρGaloisRep ℚ k V.IsIrreducibleGaloisRep.IsIrreducible.{uK, u_4, u_7} {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) : PropIrreducibility of a Galois representation over a field. )
  (hρGaloisRepresentation.IsHardlyRamified hpodd hV ρ :
    GaloisRepresentation.IsHardlyRamifiedGaloisRepresentation.IsHardlyRamified.{u, u_1} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓOdd : Odd ℓ) {R : Type u} [CommRing R]
  [TopologicalSpace R] [IsTopologicalRing R] [IsLocalRing R] [Algebra ℤ_[ℓ] R] {V : Type u_1} [AddCommGroup V]
  [Module R V] [Module.Finite R V] [Module.Free R V] (hdim : Module.rank R V = 2) (ρ : GaloisRep ℚ R V) : PropLet `R` be a compact Hausdorff local topological ring (for example any complete Noetherian
local ring with the maximal ideal-adic topology) having finite residue field of
characteristic `ℓ > 2`, and let `ρ : Gal(Qbar/Q) → GL_2(R)` be a continuous 2-dimensional
representation. We say that `ρ` is *hardly ramified* if it has cyclotomic determinant, is
unramified outside `2ℓ`, flat at `ℓ` and upper-triangular at 2 with a 1-dimensional quotient which
is unramified and whose square is trivial. 
      hpoddOdd p hVModule.rank k V = 2 ρGaloisRep ℚ k V) :
  ∃ RType u xCommRing R,
    ∃ (x_1IsLocalRing R : IsLocalRingIsLocalRing.{u_1} (R : Type u_1) [Semiring R] : PropA semiring is local if it is nontrivial and `a` or `b` is a unit whenever `a + b = 1`.
Note that `IsLocalRing` is a predicate.  RType u),
      ∃ x_2TopologicalSpace R,
        ∃ (x_3IsTopologicalRing R : IsTopologicalRingIsTopologicalRing.{u_1} (R : Type u_1) [TopologicalSpace R] [NonUnitalNonAssocRing R] : PropA topological ring is a ring `R` where addition, multiplication and negation are continuous.

If `R` is a (unital) ring, then continuity of negation can be derived from continuity of
multiplication as it is multiplication with `-1`. (See
`IsTopologicalSemiring.continuousNeg_of_mul` and
`topological_semiring.to_topological_add_group`)  RType u),
          ∃ x_4Algebra ℤ_[p] R,
            ∃ (_ :
              IsLocalHomIsLocalHom.{u_2, u_3, u_5} {R : Type u_2} {S : Type u_3} {F : Type u_5} [Monoid R] [Monoid S] [FunLike F R S] (f : F) :
  PropA map `f` between monoids is *local* if any `a` in the domain is a unit
whenever `f a` is a unit. See `IsLocalRing.local_hom_TFAE` for other equivalent
definitions in the local ring case - from where this concept originates, but it is useful in
other contexts, so we allow this generalisation in mathlib. 
                (algebraMapalgebraMap.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* AEmbedding `R →+* A` given by `Algebra` structure.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u))
              (_ : Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u)
              (_ : Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u) (_
              : IsModuleTopologyIsModuleTopology.{u_1, u_2} (R : Type u_1) [TopologicalSpace R] (A : Type u_2) [Add A] [SMul R A]
  [τA : TopologicalSpace A] : PropA class asserting that the topology on a module over a topological ring `R` is
the module topology. See `moduleTopology` for more discussion of the module topology.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u),
              ∃ x_9Algebra R k,
                ∃ (_ :
                  IsScalarTowerIsScalarTower.{u_9, u_10, u_11} (M : Type u_9) (N : Type u_10) (α : Type u_11) [SMul M N] [SMul N α] [SMul M α] : PropAn instance of `IsScalarTower M N α` states that the multiplicative
action of `M` on `α` is determined by the multiplicative actions of `M` on `N`
and `N` on `α`.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u kType u)
                  (x_11ContinuousSMul R k :
                  ContinuousSMulContinuousSMul.{u_1, u_2} (M : Type u_1) (X : Type u_2) [SMul M X] [TopologicalSpace M] [TopologicalSpace X] : PropClass `ContinuousSMul M X` says that the scalar multiplication `(•) : M → X → X`
is continuous in both arguments. We use the same class for all kinds of multiplicative actions,
including (semi)modules and algebras.  RType u kType u),
                  ∃ WType v x_12AddCommGroup W x_13Module R W,
                    ∃ (x_14Module.Finite R W :
                      Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  RType u WType v)
                      (x_15Module.Free R W :
                      Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  RType u WType v) (hWModule.rank R W = 2
                      :
                      Module.rankModule.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Cardinal.{u_2}The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).


[Stacks Tag 09G3](https://stacks.math.columbia.edu/tag/09G3) (first part) RType u WType v =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
                        2),
                      ∃ σGaloisRep ℚ R W rTensorProduct R k W ≃ₗ[k] V,
                        GaloisRepresentation.IsHardlyRamifiedGaloisRepresentation.IsHardlyRamified.{u, u_1} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓOdd : Odd ℓ) {R : Type u} [CommRing R]
  [TopologicalSpace R] [IsTopologicalRing R] [IsLocalRing R] [Algebra ℤ_[ℓ] R] {V : Type u_1} [AddCommGroup V]
  [Module R V] [Module.Finite R V] [Module.Free R V] (hdim : Module.rank R V = 2) (ρ : GaloisRep ℚ R V) : PropLet `R` be a compact Hausdorff local topological ring (for example any complete Noetherian
local ring with the maximal ideal-adic topology) having finite residue field of
characteristic `ℓ > 2`, and let `ρ : Gal(Qbar/Q) → GL_2(R)` be a continuous 2-dimensional
representation. We say that `ρ` is *hardly ramified* if it has cyclotomic determinant, is
unramified outside `2ℓ`, flat at `ℓ` and upper-triangular at 2 with a 1-dimensional quotient which
is unramified and whose square is trivial. 
                            hpoddOdd p hWModule.rank R W = 2 σGaloisRep ℚ R W ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
                          (GaloisRep.baseChangeGaloisRep.baseChange.{uK, u_2, u_3, u_4} {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`. 
                                  kType u
                                  σGaloisRep ℚ R W).conjGaloisRep.conj.{uK, u_2, u_4, u_5} {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 NWe can conjugate a galois rep by a linear isomorphism on the space. 
                              rTensorProduct R k W ≃ₗ[k] V =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
                            ρGaloisRep ℚ k V
    An irreducible mod p hardly ramified representation lifts to a p-adic one.
    contains sorry in proof
Proof

This theorem is formalized in Lean under the attached declaration.

Next we claim that a hardly ramified \ell-adic representation spreads out to a compatible family of hardly ramified q-adic representations for all odd primes q. Note that we have not made a definition of a hardly ramified 2-adic representation.

Theorem3.6
Group: Reducibility of p -torsion of the Frey curve. (7)
Hover another entry in this group to preview it.
Preview
Definition 3.1
Blueprint label
  • hardly_ramified
Group
  • Reducibility of p -torsion of the Frey curve.
⚠L∃∀Nused by 1

Definition 3.1 If \ell \ge 3 is prime, K is a finite extension of \Q_\ell with integers \mathcal{O} and if \rho : \GQ \to \GL_2(\mathcal{O}) is a hardly ramified representation whose reduction is irreducible, then there exists a number field M and, for each finite place \mu of M of characteristic prime to 2, with completion M_\mu having integer ring R_\mu, a hardly ramified semisimple representation \rho_\mu : \GQ \to \GL_2(R_\mu) (by which we mean the generic fibre is semisimple), with the following properties:

  • There is some \lambda\mid\ell of M such that \rho_\lambda\cong\rho, the isomorphism happening over some appropriate local field containing a copy of M_\lambda and a copy of K

  • If \mu_1 and \mu_2 are two finite places of M with odd residue characteristics m_1 and m_2, and if p\nmid 2m_1m_2 is prime, then \rho_{\mu_1} and \rho_{\mu_2} are both unramified at p and the characteristic polynomials \rho_{\mu_1}(\Frob_p) and \rho_{\mu_2}(\Frob_p) lie in M[X] and are equal

Code for Theorem3.6●1 theorem, incomplete
  • theorem GaloisRepresentation.IsHardlyRamified.mem_isCompatible.{u, v} {pℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  (hpoddOdd p : OddOdd.{u_2} {α : Type u_2} [Semiring α] (a : α) : PropAn element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  pℕ) [hpFact (Nat.Prime p) : FactFact (p : Prop) : PropWrapper for adding elementary propositions to the type class systems.
Warning: this can easily be abused. See the rest of this docstring for details.

Certain propositions should not be treated as a class globally,
but sometimes it is very convenient to be able to use the type class system
in specific circumstances.

For example, `ZMod p` is a field if and only if `p` is a prime number.
In order to be able to find this field instance automatically by type class search,
we have to turn `p.prime` into an instance implicit assumption.

On the other hand, making `Nat.prime` a class would require a major refactoring of the library,
and it is questionable whether making `Nat.prime` a class is desirable at all.
The compromise is to add the assumption `[Fact p.prime]` to `ZMod.field`.

In particular, this class is not intended for turning the type class system
into an automated theorem prover for first-order logic.  (Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  pℕ)] {RType u : Type uA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  RType u]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u] [IsDomainIsDomain.{u} (α : Type u) [Semiring α] : PropA domain is a nontrivial semiring such that multiplication by a nonzero element
is cancellative on both sides. In other words, a nontrivial semiring `R` satisfying
`∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c` and
`∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c`.

This is implemented as a mixin for `Semiring α`.
To obtain an integral domain use `[CommRing α] [IsDomain α]`.  RType u] [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u]
  [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  RType u] [IsTopologicalRingIsTopologicalRing.{u_1} (R : Type u_1) [TopologicalSpace R] [NonUnitalNonAssocRing R] : PropA topological ring is a ring `R` where addition, multiplication and negation are continuous.

If `R` is a (unital) ring, then continuity of negation can be derived from continuity of
multiplication as it is multiplication with `-1`. (See
`IsTopologicalSemiring.continuousNeg_of_mul` and
`topological_semiring.to_topological_add_group`)  RType u] [IsLocalRingIsLocalRing.{u_1} (R : Type u_1) [Semiring R] : PropA semiring is local if it is nontrivial and `a` or `b` is a unit whenever `a + b = 1`.
Note that `IsLocalRing` is a predicate.  RType u]
  [IsModuleTopologyIsModuleTopology.{u_1, u_2} (R : Type u_1) [TopologicalSpace R] (A : Type u_2) [Add A] [SMul R A]
  [τA : TopologicalSpace A] : PropA class asserting that the topology on a module over a topological ring `R` is
the module topology. See `moduleTopology` for more discussion of the module topology.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u] {VType v : Type vA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  VType v] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  RType u VType v]
  [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  RType u VType v] [Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  RType u VType v] (hvModule.rank R V = 2 : Module.rankModule.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Cardinal.{u_2}The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).


[Stacks Tag 09G3](https://stacks.math.columbia.edu/tag/09G3) (first part) RType u VType v =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 2)
  {ρGaloisRep ℚ R V : GaloisRepGaloisRep.{uK, u_2, u_4} (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`.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 RType u VType v}
  (hρGaloisRepresentation.IsHardlyRamified hpodd hv ρ : GaloisRepresentation.IsHardlyRamifiedGaloisRepresentation.IsHardlyRamified.{u, u_1} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓOdd : Odd ℓ) {R : Type u} [CommRing R]
  [TopologicalSpace R] [IsTopologicalRing R] [IsLocalRing R] [Algebra ℤ_[ℓ] R] {V : Type u_1} [AddCommGroup V]
  [Module R V] [Module.Finite R V] [Module.Free R V] (hdim : Module.rank R V = 2) (ρ : GaloisRep ℚ R V) : PropLet `R` be a compact Hausdorff local topological ring (for example any complete Noetherian
local ring with the maximal ideal-adic topology) having finite residue field of
characteristic `ℓ > 2`, and let `ρ : Gal(Qbar/Q) → GL_2(R)` be a continuous 2-dimensional
representation. We say that `ρ` is *hardly ramified* if it has cyclotomic determinant, is
unramified outside `2ℓ`, flat at `ℓ` and upper-triangular at 2 with a 1-dimensional quotient which
is unramified and whose square is trivial.  hpoddOdd p hvModule.rank R V = 2 ρGaloisRep ℚ R V) :
  ∃ EType v xField E,
    ∃ (x_1NumberField E : NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  EType v),
      ∃ σGaloisRepFamily ℚ E 2,
        σGaloisRepFamily ℚ E 2.isCompatibleGaloisRepFamily.isCompatible.{u_1, u_2} {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [Field E]
  [NumberField E] {d : ℕ} (ρ : GaloisRepFamily K E d) : PropA family `ρ_λ` of `E_λ`-adic Galois representations `GaloisRepFamily K E d` of the
absolute Galois group of a number field `K` is *compatible* if there is a finite set `S` of
finite places of `K` and, for each finite place `v` of `K` not in `S`, a monic
degree `d` polynomial `P_v` with coefficients in `E`, such that if
`v` and `λ` do not lie above the same rational prime then `ρ_λ` is unramified at `v`
and `P_v` is the characteristic polynomial of `ρ_λ(Frob_v)`, where `Frob_v` denotes
an arithmetic Frobenius element.

This is the weakest possible concept of a compatible family but it will
suffice for our needs.
 ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
          (∀ {ℓℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} (hℓFact (Nat.Prime ℓ) : FactFact (p : Prop) : PropWrapper for adding elementary propositions to the type class systems.
Warning: this can easily be abused. See the rest of this docstring for details.

Certain propositions should not be treated as a class globally,
but sometimes it is very convenient to be able to use the type class system
in specific circumstances.

For example, `ZMod p` is a field if and only if `p` is a prime number.
In order to be able to find this field instance automatically by type class search,
we have to turn `p.prime` into an instance implicit assumption.

On the other hand, making `Nat.prime` a class would require a major refactoring of the library,
and it is questionable whether making `Nat.prime` a class is desirable at all.
The compromise is to add the assumption `[Fact p.prime]` to `ZMod.field`.

In particular, this class is not intended for turning the type class system
into an automated theorem prover for first-order logic.  (Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  ℓℕ)) (hℓoddOdd ℓ : OddOdd.{u_2} {α : Type u_2} [Semiring α] (a : α) : PropAn element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  ℓℕ)
              (φE →+* AlgebraicClosure ℚ_[ℓ] : EType v →+*RingHom.{u_5, u_6} (α : Type u_5) (β : Type u_6) [NonAssocSemiring α] [NonAssocSemiring β] : Type (max u_5 u_6)Bundled semiring homomorphisms; use this for bundled ring homomorphisms too.

This extends from both `MonoidHom` and `MonoidWithZeroHom` in order to put the fields in a
sensible order, even though `MonoidWithZeroHom` already extends `MonoidHom`.  AlgebraicClosureAlgebraicClosure.{u} (k : Type u) [Field k] : Type uThe canonical algebraic closure of a field, the direct limit of adding roots to the field for
each polynomial over the field.  ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
ℓℕ]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
),
              ∃ AType u xCommRing A x_2TopologicalSpace A,
                ∃ (x_3IsTopologicalRing A : IsTopologicalRingIsTopologicalRing.{u_1} (R : Type u_1) [TopologicalSpace R] [NonUnitalNonAssocRing R] : PropA topological ring is a ring `R` where addition, multiplication and negation are continuous.

If `R` is a (unital) ring, then continuity of negation can be derived from continuity of
multiplication as it is multiplication with `-1`. (See
`IsTopologicalSemiring.continuousNeg_of_mul` and
`topological_semiring.to_topological_add_group`)  AType u) (x_4IsLocalRing A : IsLocalRingIsLocalRing.{u_1} (R : Type u_1) [Semiring R] : PropA semiring is local if it is nontrivial and `a` or `b` is a unit whenever `a + b = 1`.
Note that `IsLocalRing` is a predicate.  AType u),
                  ∃ x_5Algebra ℤ_[ℓ] A,
                    ∃ (_ : Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. ℓℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  AType u) (_ :
                      Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. ℓℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  AType u) (_ : IsDomainIsDomain.{u} (α : Type u) [Semiring α] : PropA domain is a nontrivial semiring such that multiplication by a nonzero element
is cancellative on both sides. In other words, a nontrivial semiring `R` satisfying
`∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c` and
`∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c`.

This is implemented as a mixin for `Semiring α`.
To obtain an integral domain use `[CommRing α] [IsDomain α]`.  AType u),
                      ∃ x_9Algebra A (AlgebraicClosure ℚ_[ℓ]),
                        ∃ (_ :
                          IsScalarTowerIsScalarTower.{u_9, u_10, u_11} (M : Type u_9) (N : Type u_10) (α : Type u_11) [SMul M N] [SMul N α] [SMul M α] : PropAn instance of `IsScalarTower M N α` states that the multiplicative
action of `M` on `α` is determined by the multiplicative actions of `M` on `N`
and `N` on `α`.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. ℓℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  AType u
                            (AlgebraicClosureAlgebraicClosure.{u} (k : Type u) [Field k] : Type uThe canonical algebraic closure of a field, the direct limit of adding roots to the field for
each polynomial over the field.  ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
ℓℕ]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
))
                          (_ : IsModuleTopologyIsModuleTopology.{u_1, u_2} (R : Type u_1) [TopologicalSpace R] (A : Type u_2) [Add A] [SMul R A]
  [τA : TopologicalSpace A] : PropA class asserting that the topology on a module over a topological ring `R` is
the module topology. See `moduleTopology` for more discussion of the module topology.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. ℓℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  AType u) (x_12ContinuousSMul A (AlgebraicClosure ℚ_[ℓ]) :
                          ContinuousSMulContinuousSMul.{u_1, u_2} (M : Type u_1) (X : Type u_2) [SMul M X] [TopologicalSpace M] [TopologicalSpace X] : PropClass `ContinuousSMul M X` says that the scalar multiplication `(•) : M → X → X`
is continuous in both arguments. We use the same class for all kinds of multiplicative actions,
including (semi)modules and algebras.  AType u (AlgebraicClosureAlgebraicClosure.{u} (k : Type u) [Field k] : Type uThe canonical algebraic closure of a field, the direct limit of adding roots to the field for
each polynomial over the field.  ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
ℓℕ]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
)),
                          ∃ WType v x_13AddCommGroup W x_14Module A W,
                            ∃ (x_15Module.Finite A W : Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  AType u WType v) (x_16Module.Free A W :
                              Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  AType u WType v) (hWModule.rank A W = 2 :
                              Module.rankModule.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Cardinal.{u_2}The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).


[Stacks Tag 09G3](https://stacks.math.columbia.edu/tag/09G3) (first part) AType u WType v =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 2),
                              ∃ τGaloisRep ℚ A W rTensorProduct A (AlgebraicClosure ℚ_[ℓ]) W ≃ₗ[AlgebraicClosure ℚ_[ℓ]] Fin 2 → AlgebraicClosure ℚ_[ℓ],
                                GaloisRepresentation.IsHardlyRamifiedGaloisRepresentation.IsHardlyRamified.{u, u_1} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓOdd : Odd ℓ) {R : Type u} [CommRing R]
  [TopologicalSpace R] [IsTopologicalRing R] [IsLocalRing R] [Algebra ℤ_[ℓ] R] {V : Type u_1} [AddCommGroup V]
  [Module R V] [Module.Finite R V] [Module.Free R V] (hdim : Module.rank R V = 2) (ρ : GaloisRep ℚ R V) : PropLet `R` be a compact Hausdorff local topological ring (for example any complete Noetherian
local ring with the maximal ideal-adic topology) having finite residue field of
characteristic `ℓ > 2`, and let `ρ : Gal(Qbar/Q) → GL_2(R)` be a continuous 2-dimensional
representation. We say that `ρ` is *hardly ramified* if it has cyclotomic determinant, is
unramified outside `2ℓ`, flat at `ℓ` and upper-triangular at 2 with a 1-dimensional quotient which
is unramified and whose square is trivial. 
                                    hℓoddOdd ℓ hWModule.rank A W = 2 τGaloisRep ℚ A W ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
                                  (GaloisRep.baseChangeGaloisRep.baseChange.{uK, u_2, u_3, u_4} {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`. 
                                          (AlgebraicClosureAlgebraicClosure.{u} (k : Type u) [Field k] : Type uThe canonical algebraic closure of a field, the direct limit of adding roots to the field for
each polynomial over the field.  ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
ℓℕ]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
)
                                          τGaloisRep ℚ A W).conjGaloisRep.conj.{uK, u_2, u_4, u_5} {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 NWe can conjugate a galois rep by a linear isomorphism on the space. 
                                      rTensorProduct A (AlgebraicClosure ℚ_[ℓ]) W ≃ₗ[AlgebraicClosure ℚ_[ℓ]] Fin 2 → AlgebraicClosure ℚ_[ℓ] =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
                                    σGaloisRepFamily ℚ E 2 hℓFact (Nat.Prime ℓ) φE →+* AlgebraicClosure ℚ_[ℓ]) ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
            ∃ x_2Algebra R (AlgebraicClosure ℚ_[p]),
              ∃ (x_3ContinuousSMul R (AlgebraicClosure ℚ_[p]) : ContinuousSMulContinuousSMul.{u_1, u_2} (M : Type u_1) (X : Type u_2) [SMul M X] [TopologicalSpace M] [TopologicalSpace X] : PropClass `ContinuousSMul M X` says that the scalar multiplication `(•) : M → X → X`
is continuous in both arguments. We use the same class for all kinds of multiplicative actions,
including (semi)modules and algebras.  RType u (AlgebraicClosureAlgebraicClosure.{u} (k : Type u) [Field k] : Type uThe canonical algebraic closure of a field, the direct limit of adding roots to the field for
each polynomial over the field.  ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
pℕ]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
)),
                ∃ ψE →+* AlgebraicClosure ℚ_[p] r'TensorProduct R (AlgebraicClosure ℚ_[p]) V ≃ₗ[AlgebraicClosure ℚ_[p]] Fin 2 → AlgebraicClosure ℚ_[p],
                  (GaloisRep.baseChangeGaloisRep.baseChange.{uK, u_2, u_3, u_4} {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`.  (AlgebraicClosureAlgebraicClosure.{u} (k : Type u) [Field k] : Type uThe canonical algebraic closure of a field, the direct limit of adding roots to the field for
each polynomial over the field.  ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
pℕ]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
) ρGaloisRep ℚ R V).conjGaloisRep.conj.{uK, u_2, u_4, u_5} {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 NWe can conjugate a galois rep by a linear isomorphism on the space. 
                      r'TensorProduct R (AlgebraicClosure ℚ_[p]) V ≃ₗ[AlgebraicClosure ℚ_[p]] Fin 2 → AlgebraicClosure ℚ_[p] =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
                    σGaloisRepFamily ℚ E 2 hpFact (Nat.Prime p) ψE →+* AlgebraicClosure ℚ_[p]
    theorem GaloisRepresentation.IsHardlyRamified.mem_isCompatible.{u,
    v}
  {pℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} (hpoddOdd p : OddOdd.{u_2} {α : Type u_2} [Semiring α] (a : α) : PropAn element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  pℕ)
  [hpFact (Nat.Prime p) : FactFact (p : Prop) : PropWrapper for adding elementary propositions to the type class systems.
Warning: this can easily be abused. See the rest of this docstring for details.

Certain propositions should not be treated as a class globally,
but sometimes it is very convenient to be able to use the type class system
in specific circumstances.

For example, `ZMod p` is a field if and only if `p` is a prime number.
In order to be able to find this field instance automatically by type class search,
we have to turn `p.prime` into an instance implicit assumption.

On the other hand, making `Nat.prime` a class would require a major refactoring of the library,
and it is questionable whether making `Nat.prime` a class is desirable at all.
The compromise is to add the assumption `[Fact p.prime]` to `ZMod.field`.

In particular, this class is not intended for turning the type class system
into an automated theorem prover for first-order logic.  (Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  pℕ)] {RType u : Type uA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  RType u] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u]
  [IsDomainIsDomain.{u} (α : Type u) [Semiring α] : PropA domain is a nontrivial semiring such that multiplication by a nonzero element
is cancellative on both sides. In other words, a nontrivial semiring `R` satisfying
`∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c` and
`∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c`.

This is implemented as a mixin for `Semiring α`.
To obtain an integral domain use `[CommRing α] [IsDomain α]`.  RType u] [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u]
  [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  RType u]
  [IsTopologicalRingIsTopologicalRing.{u_1} (R : Type u_1) [TopologicalSpace R] [NonUnitalNonAssocRing R] : PropA topological ring is a ring `R` where addition, multiplication and negation are continuous.

If `R` is a (unital) ring, then continuity of negation can be derived from continuity of
multiplication as it is multiplication with `-1`. (See
`IsTopologicalSemiring.continuousNeg_of_mul` and
`topological_semiring.to_topological_add_group`)  RType u] [IsLocalRingIsLocalRing.{u_1} (R : Type u_1) [Semiring R] : PropA semiring is local if it is nontrivial and `a` or `b` is a unit whenever `a + b = 1`.
Note that `IsLocalRing` is a predicate.  RType u]
  [IsModuleTopologyIsModuleTopology.{u_1, u_2} (R : Type u_1) [TopologicalSpace R] (A : Type u_2) [Add A] [SMul R A]
  [τA : TopologicalSpace A] : PropA class asserting that the topology on a module over a topological ring `R` is
the module topology. See `moduleTopology` for more discussion of the module topology.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. pℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u] {VType v : Type vA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  VType v] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  RType u VType v]
  [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  RType u VType v] [Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  RType u VType v]
  (hvModule.rank R V = 2 : Module.rankModule.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Cardinal.{u_2}The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).


[Stacks Tag 09G3](https://stacks.math.columbia.edu/tag/09G3) (first part) RType u VType v =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 2)
  {ρGaloisRep ℚ R V : GaloisRepGaloisRep.{uK, u_2, u_4} (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`.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 RType u VType v}
  (hρGaloisRepresentation.IsHardlyRamified hpodd hv ρ :
    GaloisRepresentation.IsHardlyRamifiedGaloisRepresentation.IsHardlyRamified.{u, u_1} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓOdd : Odd ℓ) {R : Type u} [CommRing R]
  [TopologicalSpace R] [IsTopologicalRing R] [IsLocalRing R] [Algebra ℤ_[ℓ] R] {V : Type u_1} [AddCommGroup V]
  [Module R V] [Module.Finite R V] [Module.Free R V] (hdim : Module.rank R V = 2) (ρ : GaloisRep ℚ R V) : PropLet `R` be a compact Hausdorff local topological ring (for example any complete Noetherian
local ring with the maximal ideal-adic topology) having finite residue field of
characteristic `ℓ > 2`, and let `ρ : Gal(Qbar/Q) → GL_2(R)` be a continuous 2-dimensional
representation. We say that `ρ` is *hardly ramified* if it has cyclotomic determinant, is
unramified outside `2ℓ`, flat at `ℓ` and upper-triangular at 2 with a 1-dimensional quotient which
is unramified and whose square is trivial. 
      hpoddOdd p hvModule.rank R V = 2 ρGaloisRep ℚ R V) :
  ∃ EType v xField E,
    ∃ (x_1NumberField E : NumberFieldNumberField.{u_1} (K : Type u_1) [Field K] : PropA number field is a field which has characteristic zero and is finite
dimensional over ℚ.  EType v),
      ∃ σGaloisRepFamily ℚ E 2,
        σGaloisRepFamily ℚ E 2.isCompatibleGaloisRepFamily.isCompatible.{u_1, u_2} {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [Field E]
  [NumberField E] {d : ℕ} (ρ : GaloisRepFamily K E d) : PropA family `ρ_λ` of `E_λ`-adic Galois representations `GaloisRepFamily K E d` of the
absolute Galois group of a number field `K` is *compatible* if there is a finite set `S` of
finite places of `K` and, for each finite place `v` of `K` not in `S`, a monic
degree `d` polynomial `P_v` with coefficients in `E`, such that if
`v` and `λ` do not lie above the same rational prime then `ρ_λ` is unramified at `v`
and `P_v` is the characteristic polynomial of `ρ_λ(Frob_v)`, where `Frob_v` denotes
an arithmetic Frobenius element.

This is the weakest possible concept of a compatible family but it will
suffice for our needs.
 ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
          (∀ {ℓℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
              (hℓFact (Nat.Prime ℓ) : FactFact (p : Prop) : PropWrapper for adding elementary propositions to the type class systems.
Warning: this can easily be abused. See the rest of this docstring for details.

Certain propositions should not be treated as a class globally,
but sometimes it is very convenient to be able to use the type class system
in specific circumstances.

For example, `ZMod p` is a field if and only if `p` is a prime number.
In order to be able to find this field instance automatically by type class search,
we have to turn `p.prime` into an instance implicit assumption.

On the other hand, making `Nat.prime` a class would require a major refactoring of the library,
and it is questionable whether making `Nat.prime` a class is desirable at all.
The compromise is to add the assumption `[Fact p.prime]` to `ZMod.field`.

In particular, this class is not intended for turning the type class system
into an automated theorem prover for first-order logic.  (Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  ℓℕ))
              (hℓoddOdd ℓ : OddOdd.{u_2} {α : Type u_2} [Semiring α] (a : α) : PropAn element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  ℓℕ)
              (φE →+* AlgebraicClosure ℚ_[ℓ] :
                EType v →+*RingHom.{u_5, u_6} (α : Type u_5) (β : Type u_6) [NonAssocSemiring α] [NonAssocSemiring β] : Type (max u_5 u_6)Bundled semiring homomorphisms; use this for bundled ring homomorphisms too.

This extends from both `MonoidHom` and `MonoidWithZeroHom` in order to put the fields in a
sensible order, even though `MonoidWithZeroHom` already extends `MonoidHom`. 
                  AlgebraicClosureAlgebraicClosure.{u} (k : Type u) [Field k] : Type uThe canonical algebraic closure of a field, the direct limit of adding roots to the field for
each polynomial over the field.  ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
ℓℕ]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
),
              ∃ AType u xCommRing A x_2TopologicalSpace A,
                ∃ (x_3IsTopologicalRing A :
                  IsTopologicalRingIsTopologicalRing.{u_1} (R : Type u_1) [TopologicalSpace R] [NonUnitalNonAssocRing R] : PropA topological ring is a ring `R` where addition, multiplication and negation are continuous.

If `R` is a (unital) ring, then continuity of negation can be derived from continuity of
multiplication as it is multiplication with `-1`. (See
`IsTopologicalSemiring.continuousNeg_of_mul` and
`topological_semiring.to_topological_add_group`)  AType u)
                  (x_4IsLocalRing A : IsLocalRingIsLocalRing.{u_1} (R : Type u_1) [Semiring R] : PropA semiring is local if it is nontrivial and `a` or `b` is a unit whenever `a + b = 1`.
Note that `IsLocalRing` is a predicate.  AType u),
                  ∃ x_5Algebra ℤ_[ℓ] A,
                    ∃ (_ :
                      Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. ℓℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. 
                        AType u)
                      (_ :
                      Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. ℓℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  AType u)
                      (_ : IsDomainIsDomain.{u} (α : Type u) [Semiring α] : PropA domain is a nontrivial semiring such that multiplication by a nonzero element
is cancellative on both sides. In other words, a nontrivial semiring `R` satisfying
`∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c` and
`∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c`.

This is implemented as a mixin for `Semiring α`.
To obtain an integral domain use `[CommRing α] [IsDomain α]`.  AType u),
                      ∃ x_9Algebra A (AlgebraicClosure ℚ_[ℓ]),
                        ∃ (_ :
                          IsScalarTowerIsScalarTower.{u_9, u_10, u_11} (M : Type u_9) (N : Type u_10) (α : Type u_11) [SMul M N] [SMul N α] [SMul M α] : PropAn instance of `IsScalarTower M N α` states that the multiplicative
action of `M` on `α` is determined by the multiplicative actions of `M` on `N`
and `N` on `α`. 
                            ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. ℓℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  AType u
                            (AlgebraicClosureAlgebraicClosure.{u} (k : Type u) [Field k] : Type uThe canonical algebraic closure of a field, the direct limit of adding roots to the field for
each polynomial over the field. 
                              ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
ℓℕ]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
))
                          (_ :
                          IsModuleTopologyIsModuleTopology.{u_1, u_2} (R : Type u_1) [TopologicalSpace R] (A : Type u_2) [Add A] [SMul R A]
  [τA : TopologicalSpace A] : PropA class asserting that the topology on a module over a topological ring `R` is
the module topology. See `moduleTopology` for more discussion of the module topology. 
                            ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. ℓℕ]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  AType u)
                          (x_12ContinuousSMul A (AlgebraicClosure ℚ_[ℓ]) :
                          ContinuousSMulContinuousSMul.{u_1, u_2} (M : Type u_1) (X : Type u_2) [SMul M X] [TopologicalSpace M] [TopologicalSpace X] : PropClass `ContinuousSMul M X` says that the scalar multiplication `(•) : M → X → X`
is continuous in both arguments. We use the same class for all kinds of multiplicative actions,
including (semi)modules and algebras.  AType u
                            (AlgebraicClosureAlgebraicClosure.{u} (k : Type u) [Field k] : Type uThe canonical algebraic closure of a field, the direct limit of adding roots to the field for
each polynomial over the field. 
                              ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
ℓℕ]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
)),
                          ∃ WType v x_13AddCommGroup W x_14Module A W,
                            ∃ (x_15Module.Finite A W :
                              Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module. 
                                AType u WType v)
                              (x_16Module.Free A W :
                              Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free. 
                                AType u WType v)
                              (hWModule.rank A W = 2 :
                              Module.rankModule.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Cardinal.{u_2}The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).


[Stacks Tag 09G3](https://stacks.math.columbia.edu/tag/09G3) (first part)
                                  AType u WType v =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
                                2),
                              ∃ τGaloisRep ℚ A W rTensorProduct A (AlgebraicClosure ℚ_[ℓ]) W ≃ₗ[AlgebraicClosure ℚ_[ℓ]] Fin 2 → AlgebraicClosure ℚ_[ℓ],
                                GaloisRepresentation.IsHardlyRamifiedGaloisRepresentation.IsHardlyRamified.{u, u_1} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓOdd : Odd ℓ) {R : Type u} [CommRing R]
  [TopologicalSpace R] [IsTopologicalRing R] [IsLocalRing R] [Algebra ℤ_[ℓ] R] {V : Type u_1} [AddCommGroup V]
  [Module R V] [Module.Finite R V] [Module.Free R V] (hdim : Module.rank R V = 2) (ρ : GaloisRep ℚ R V) : PropLet `R` be a compact Hausdorff local topological ring (for example any complete Noetherian
local ring with the maximal ideal-adic topology) having finite residue field of
characteristic `ℓ > 2`, and let `ρ : Gal(Qbar/Q) → GL_2(R)` be a continuous 2-dimensional
representation. We say that `ρ` is *hardly ramified* if it has cyclotomic determinant, is
unramified outside `2ℓ`, flat at `ℓ` and upper-triangular at 2 with a 1-dimensional quotient which
is unramified and whose square is trivial. 
                                    hℓoddOdd ℓ
                                    hWModule.rank A W = 2 τGaloisRep ℚ A W ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
                                  (GaloisRep.baseChangeGaloisRep.baseChange.{uK, u_2, u_3, u_4} {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`. 
                                          (AlgebraicClosureAlgebraicClosure.{u} (k : Type u) [Field k] : Type uThe canonical algebraic closure of a field, the direct limit of adding roots to the field for
each polynomial over the field. 
                                            ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
ℓℕ]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
)
                                          τGaloisRep ℚ A W).conjGaloisRep.conj.{uK, u_2, u_4, u_5} {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 NWe can conjugate a galois rep by a linear isomorphism on the space. 
                                      rTensorProduct A (AlgebraicClosure ℚ_[ℓ]) W ≃ₗ[AlgebraicClosure ℚ_[ℓ]] Fin 2 → AlgebraicClosure ℚ_[ℓ] =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
                                    σGaloisRepFamily ℚ E 2 hℓFact (Nat.Prime ℓ)
                                      φE →+* AlgebraicClosure ℚ_[ℓ]) ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
            ∃ x_2Algebra R (AlgebraicClosure ℚ_[p]),
              ∃ (x_3ContinuousSMul R (AlgebraicClosure ℚ_[p]) :
                ContinuousSMulContinuousSMul.{u_1, u_2} (M : Type u_1) (X : Type u_2) [SMul M X] [TopologicalSpace M] [TopologicalSpace X] : PropClass `ContinuousSMul M X` says that the scalar multiplication `(•) : M → X → X`
is continuous in both arguments. We use the same class for all kinds of multiplicative actions,
including (semi)modules and algebras.  RType u
                  (AlgebraicClosureAlgebraicClosure.{u} (k : Type u) [Field k] : Type uThe canonical algebraic closure of a field, the direct limit of adding roots to the field for
each polynomial over the field. 
                    ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
pℕ]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
)),
                ∃ ψE →+* AlgebraicClosure ℚ_[p] r'TensorProduct R (AlgebraicClosure ℚ_[p]) V ≃ₗ[AlgebraicClosure ℚ_[p]] Fin 2 → AlgebraicClosure ℚ_[p],
                  (GaloisRep.baseChangeGaloisRep.baseChange.{uK, u_2, u_3, u_4} {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`. 
                          (AlgebraicClosureAlgebraicClosure.{u} (k : Type u) [Field k] : Type uThe canonical algebraic closure of a field, the direct limit of adding roots to the field for
each polynomial over the field. 
                            ℚ_[Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
pℕ]Padic (p : ℕ) [Fact (Nat.Prime p)] : TypeThe `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
)
                          ρGaloisRep ℚ R V).conjGaloisRep.conj.{uK, u_2, u_4, u_5} {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 NWe can conjugate a galois rep by a linear isomorphism on the space. 
                      r'TensorProduct R (AlgebraicClosure ℚ_[p]) V ≃ₗ[AlgebraicClosure ℚ_[p]] Fin 2 → AlgebraicClosure ℚ_[p] =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
                    σGaloisRepFamily ℚ E 2 hpFact (Nat.Prime p) ψE →+* AlgebraicClosure ℚ_[p]
    contains sorry in proof
Proof

This theorem is formalized in Lean under the attached declaration.

In particular, we can "move" from an irreducible hardly ramified mod \ell representation to a hardly ramified 3-adic representation, and hence to a hardly ramified mod 3 representation.

However, we can essentially completely classify the hardly ramified mod 3 Galois representations:

Theorem3.7
Group: Reducibility of p -torsion of the Frey curve. (7)
Hover another entry in this group to preview it.
Preview
Definition 3.1
Blueprint label
  • hardly_ramified
Group
  • Reducibility of p -torsion of the Frey curve.
⚠L∃∀Nused by 1

Definition 3.1 If k is a finite field of characteristic 3 and \overline{\rho} : \GQ \to \GL_2(k) is hardly ramified, then \overline{\rho} is an extension of the cyclotomic character by the trivial representation.

Code for Theorem3.7●1 theorem, incomplete
  • theorem GaloisRepresentation.IsHardlyRamified.mod_three.{u, u_1} {kType u : Type uA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 kType u] [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  kType u] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. 3]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  kType u] [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  kType u]
  [DiscreteTopologyDiscreteTopology.{u_2} (α : Type u_2) [t : TopologicalSpace α] : PropA topological space is discrete if every set is open, that is,
its topology equals the discrete topology `⊥`.  kType u] (VType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  VType u_1] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  kType u VType u_1]
  [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  kType u VType u_1] [Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  kType u VType u_1] (hVModule.rank k V = 2 : Module.rankModule.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Cardinal.{u_2}The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).


[Stacks Tag 09G3](https://stacks.math.columbia.edu/tag/09G3) (first part) kType u VType u_1 =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 2)
  {ρGaloisRep ℚ k V : GaloisRepGaloisRep.{uK, u_2, u_4} (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`.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 kType u VType u_1}
  (hρGaloisRepresentation.IsHardlyRamified ⋯ hV ρ : GaloisRepresentation.IsHardlyRamifiedGaloisRepresentation.IsHardlyRamified.{u, u_1} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓOdd : Odd ℓ) {R : Type u} [CommRing R]
  [TopologicalSpace R] [IsTopologicalRing R] [IsLocalRing R] [Algebra ℤ_[ℓ] R] {V : Type u_1} [AddCommGroup V]
  [Module R V] [Module.Finite R V] [Module.Free R V] (hdim : Module.rank R V = 2) (ρ : GaloisRep ℚ R V) : PropLet `R` be a compact Hausdorff local topological ring (for example any complete Noetherian
local ring with the maximal ideal-adic topology) having finite residue field of
characteristic `ℓ > 2`, and let `ρ : Gal(Qbar/Q) → GL_2(R)` be a continuous 2-dimensional
representation. We say that `ρ` is *hardly ramified* if it has cyclotomic determinant, is
unramified outside `2ℓ`, flat at `ℓ` and upper-triangular at 2 with a 1-dimensional quotient which
is unramified and whose square is trivial.  ⋯ hVModule.rank k V = 2 ρGaloisRep ℚ k V) :
  ∃ πV →ₗ[k] k,
    ∃ (_ : Function.SurjectiveFunction.Surjective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : PropA function `f : α → β` is called surjective if every `b : β` is equal to `f a`
for some `a : α`.  ⇑πV →ₗ[k] k),
      ∀ (gField.absoluteGaloisGroup ℚ : Field.absoluteGaloisGroupField.absoluteGaloisGroup.{u_1} (K : Type u_1) [Field K] : Type u_1The absolute Galois group of `K`, defined as the Galois group of the field extension `K^al/K`,
where `K^al` is an algebraic closure of `K`.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
) (vV : VType u_1), πV →ₗ[k] k ((ρGaloisRep ℚ k V gField.absoluteGaloisGroup ℚ) vV) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. πV →ₗ[k] k vV
    theorem GaloisRepresentation.IsHardlyRamified.mod_three.{u,
    u_1}
  {kType u : Type uA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 kType u] [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  kType u]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. 3]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  kType u] [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  kType u]
  [DiscreteTopologyDiscreteTopology.{u_2} (α : Type u_2) [t : TopologicalSpace α] : PropA topological space is discrete if every set is open, that is,
its topology equals the discrete topology `⊥`.  kType u] (VType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  VType u_1] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  kType u VType u_1]
  [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  kType u VType u_1] [Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  kType u VType u_1]
  (hVModule.rank k V = 2 : Module.rankModule.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Cardinal.{u_2}The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).


[Stacks Tag 09G3](https://stacks.math.columbia.edu/tag/09G3) (first part) kType u VType u_1 =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 2)
  {ρGaloisRep ℚ k V : GaloisRepGaloisRep.{uK, u_2, u_4} (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`.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 kType u VType u_1}
  (hρGaloisRepresentation.IsHardlyRamified ⋯ hV ρ :
    GaloisRepresentation.IsHardlyRamifiedGaloisRepresentation.IsHardlyRamified.{u, u_1} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓOdd : Odd ℓ) {R : Type u} [CommRing R]
  [TopologicalSpace R] [IsTopologicalRing R] [IsLocalRing R] [Algebra ℤ_[ℓ] R] {V : Type u_1} [AddCommGroup V]
  [Module R V] [Module.Finite R V] [Module.Free R V] (hdim : Module.rank R V = 2) (ρ : GaloisRep ℚ R V) : PropLet `R` be a compact Hausdorff local topological ring (for example any complete Noetherian
local ring with the maximal ideal-adic topology) having finite residue field of
characteristic `ℓ > 2`, and let `ρ : Gal(Qbar/Q) → GL_2(R)` be a continuous 2-dimensional
representation. We say that `ρ` is *hardly ramified* if it has cyclotomic determinant, is
unramified outside `2ℓ`, flat at `ℓ` and upper-triangular at 2 with a 1-dimensional quotient which
is unramified and whose square is trivial. 
      ⋯ hVModule.rank k V = 2 ρGaloisRep ℚ k V) :
  ∃ πV →ₗ[k] k,
    ∃ (_ : Function.SurjectiveFunction.Surjective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : PropA function `f : α → β` is called surjective if every `b : β` is equal to `f a`
for some `a : α`.  ⇑πV →ₗ[k] k),
      ∀ (gField.absoluteGaloisGroup ℚ : Field.absoluteGaloisGroupField.absoluteGaloisGroup.{u_1} (K : Type u_1) [Field K] : Type u_1The absolute Galois group of `K`, defined as the Galois group of the field extension `K^al/K`,
where `K^al` is an algebraic closure of `K`.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
)
        (vV : VType u_1), πV →ₗ[k] k ((ρGaloisRep ℚ k V gField.absoluteGaloisGroup ℚ) vV) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. πV →ₗ[k] k vV
    A mod 3 hardly ramified representation is an extension of trivial by cyclo
    contains sorry in proof
Proof

This theorem is formalized in Lean under the attached declaration.

And we can use this to essentially completely classify the hardly ramified 3-adic Galois representations:

Theorem3.8
Group: Reducibility of p -torsion of the Frey curve. (7)
Hover another entry in this group to preview it.
Preview
Definition 3.1
Blueprint label
  • hardly_ramified
Group
  • Reducibility of p -torsion of the Frey curve.
⚠L∃∀Nused by 1

Definition 3.1 Theorem 3.7 If L / \Q_3 is a finite extension with integer ring \mathcal{O}_L and \rho_3 : \GQ \to \GL_2(\mathcal{O}_L) is hardly ramified, then, viewed as a representation to \GL_2(L), one has \rho_3^{ss} = 1 \oplus \chi_3 where 1 is the trivial character and \chi_3 is the 3-adic cyclotomic character.

Code for Theorem3.8●1 theorem, incomplete
  • theorem GaloisRepresentation.IsHardlyRamified.three_adic.{u_1, u_2}
  {RType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  RType u_1] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. 3]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u_1] [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. 3]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u_1]
  [Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. 3]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u_1] [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  RType u_1] [IsTopologicalRingIsTopologicalRing.{u_1} (R : Type u_1) [TopologicalSpace R] [NonUnitalNonAssocRing R] : PropA topological ring is a ring `R` where addition, multiplication and negation are continuous.

If `R` is a (unital) ring, then continuity of negation can be derived from continuity of
multiplication as it is multiplication with `-1`. (See
`IsTopologicalSemiring.continuousNeg_of_mul` and
`topological_semiring.to_topological_add_group`)  RType u_1]
  [IsLocalRingIsLocalRing.{u_1} (R : Type u_1) [Semiring R] : PropA semiring is local if it is nontrivial and `a` or `b` is a unit whenever `a + b = 1`.
Note that `IsLocalRing` is a predicate.  RType u_1] [IsModuleTopologyIsModuleTopology.{u_1, u_2} (R : Type u_1) [TopologicalSpace R] (A : Type u_2) [Add A] [SMul R A]
  [τA : TopologicalSpace A] : PropA class asserting that the topology on a module over a topological ring `R` is
the module topology. See `moduleTopology` for more discussion of the module topology.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. 3]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u_1] (VType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  VType u_2] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  RType u_1 VType u_2] [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  RType u_1 VType u_2] [Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  RType u_1 VType u_2]
  (hVModule.rank R V = 2 : Module.rankModule.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Cardinal.{u_2}The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).


[Stacks Tag 09G3](https://stacks.math.columbia.edu/tag/09G3) (first part) RType u_1 VType u_2 =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 2) {ρGaloisRep ℚ R V : GaloisRepGaloisRep.{uK, u_2, u_4} (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`.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 RType u_1 VType u_2}
  (hρGaloisRepresentation.IsHardlyRamified ⋯ hV ρ : GaloisRepresentation.IsHardlyRamifiedGaloisRepresentation.IsHardlyRamified.{u, u_1} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓOdd : Odd ℓ) {R : Type u} [CommRing R]
  [TopologicalSpace R] [IsTopologicalRing R] [IsLocalRing R] [Algebra ℤ_[ℓ] R] {V : Type u_1} [AddCommGroup V]
  [Module R V] [Module.Finite R V] [Module.Free R V] (hdim : Module.rank R V = 2) (ρ : GaloisRep ℚ R V) : PropLet `R` be a compact Hausdorff local topological ring (for example any complete Noetherian
local ring with the maximal ideal-adic topology) having finite residue field of
characteristic `ℓ > 2`, and let `ρ : Gal(Qbar/Q) → GL_2(R)` be a continuous 2-dimensional
representation. We say that `ρ` is *hardly ramified* if it has cyclotomic determinant, is
unramified outside `2ℓ`, flat at `ℓ` and upper-triangular at 2 with a 1-dimensional quotient which
is unramified and whose square is trivial.  ⋯ hVModule.rank R V = 2 ρGaloisRep ℚ R V) (pℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
)
  (hpNat.Prime p : Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  pℕ) (hp55 ≤ p : 5 ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`). pℕ) :
  (LinearMap.traceLinearMap.trace.{u, v} (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : (M →ₗ[R] M) →ₗ[R] RTrace of an endomorphism independent of basis.  RType u_1 VType u_2)
      ((ρGaloisRep ℚ R V.toLocalGaloisRep.toLocal.{uK, u_2, u_4} {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 MGiven 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`.  hpNat.Prime p.toHeightOneSpectrumRingOfIntegersRatNat.Prime.toHeightOneSpectrumRingOfIntegersRat {p : ℕ} (hp : Nat.Prime p) :
  IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)The element of `HeightOneSpectrum (𝓞 ℚ)` associated to a prime number. )
        (Field.AbsoluteGaloisGroup.adicArithFrobField.AbsoluteGaloisGroup.adicArithFrob.{u_1} {K : Type u_1} [Field K] [NumberField K]
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
  Field.absoluteGaloisGroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)An arbitrary choice of an (arithmetic) frobenious element of a local galois group. 
          hpNat.Prime p.toHeightOneSpectrumRingOfIntegersRatNat.Prime.toHeightOneSpectrumRingOfIntegersRat {p : ℕ} (hp : Nat.Prime p) :
  IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)The element of `HeightOneSpectrum (𝓞 ℚ)` associated to a prime number. )) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    1 +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. ↑pℕ
    theorem GaloisRepresentation.IsHardlyRamified.three_adic.{u_1,
    u_2}
  {RType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  RType u_1]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. 3]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u_1]
  [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. 3]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u_1]
  [Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. 3]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u_1]
  [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  RType u_1]
  [IsTopologicalRingIsTopologicalRing.{u_1} (R : Type u_1) [TopologicalSpace R] [NonUnitalNonAssocRing R] : PropA topological ring is a ring `R` where addition, multiplication and negation are continuous.

If `R` is a (unital) ring, then continuity of negation can be derived from continuity of
multiplication as it is multiplication with `-1`. (See
`IsTopologicalSemiring.continuousNeg_of_mul` and
`topological_semiring.to_topological_add_group`)  RType u_1] [IsLocalRingIsLocalRing.{u_1} (R : Type u_1) [Semiring R] : PropA semiring is local if it is nontrivial and `a` or `b` is a unit whenever `a + b = 1`.
Note that `IsLocalRing` is a predicate.  RType u_1]
  [IsModuleTopologyIsModuleTopology.{u_1, u_2} (R : Type u_1) [TopologicalSpace R] (A : Type u_2) [Add A] [SMul R A]
  [τA : TopologicalSpace A] : PropA class asserting that the topology on a module over a topological ring `R` is
the module topology. See `moduleTopology` for more discussion of the module topology.  ℤ_[PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. 3]PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : TypeThe `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  RType u_1]
  (VType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  VType u_2]
  [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  RType u_1 VType u_2] [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  RType u_1 VType u_2]
  [Module.FreeModule.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop`Module.Free R M` is the statement that the `R`-module `M` is free.  RType u_1 VType u_2]
  (hVModule.rank R V = 2 : Module.rankModule.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Cardinal.{u_2}The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).


[Stacks Tag 09G3](https://stacks.math.columbia.edu/tag/09G3) (first part) RType u_1 VType u_2 =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 2)
  {ρGaloisRep ℚ R V : GaloisRepGaloisRep.{uK, u_2, u_4} (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`.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 RType u_1 VType u_2}
  (hρGaloisRepresentation.IsHardlyRamified ⋯ hV ρ :
    GaloisRepresentation.IsHardlyRamifiedGaloisRepresentation.IsHardlyRamified.{u, u_1} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓOdd : Odd ℓ) {R : Type u} [CommRing R]
  [TopologicalSpace R] [IsTopologicalRing R] [IsLocalRing R] [Algebra ℤ_[ℓ] R] {V : Type u_1} [AddCommGroup V]
  [Module R V] [Module.Finite R V] [Module.Free R V] (hdim : Module.rank R V = 2) (ρ : GaloisRep ℚ R V) : PropLet `R` be a compact Hausdorff local topological ring (for example any complete Noetherian
local ring with the maximal ideal-adic topology) having finite residue field of
characteristic `ℓ > 2`, and let `ρ : Gal(Qbar/Q) → GL_2(R)` be a continuous 2-dimensional
representation. We say that `ρ` is *hardly ramified* if it has cyclotomic determinant, is
unramified outside `2ℓ`, flat at `ℓ` and upper-triangular at 2 with a 1-dimensional quotient which
is unramified and whose square is trivial. 
      ⋯ hVModule.rank R V = 2 ρGaloisRep ℚ R V)
  (pℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) (hpNat.Prime p : Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  pℕ)
  (hp55 ≤ p : 5 ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`). pℕ) :
  (LinearMap.traceLinearMap.trace.{u, v} (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : (M →ₗ[R] M) →ₗ[R] RTrace of an endomorphism independent of basis.  RType u_1 VType u_2)
      ((ρGaloisRep ℚ R V.toLocalGaloisRep.toLocal.{uK, u_2, u_4} {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 MGiven 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`. 
          hpNat.Prime p.toHeightOneSpectrumRingOfIntegersRatNat.Prime.toHeightOneSpectrumRingOfIntegersRat {p : ℕ} (hp : Nat.Prime p) :
  IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)The element of `HeightOneSpectrum (𝓞 ℚ)` associated to a prime number. )
        (Field.AbsoluteGaloisGroup.adicArithFrobField.AbsoluteGaloisGroup.adicArithFrob.{u_1} {K : Type u_1} [Field K] [NumberField K]
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
  Field.absoluteGaloisGroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)An arbitrary choice of an (arithmetic) frobenious element of a local galois group. 
          hpNat.Prime p.toHeightOneSpectrumRingOfIntegersRatNat.Prime.toHeightOneSpectrumRingOfIntegersRat {p : ℕ} (hp : Nat.Prime p) :
  IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)The element of `HeightOneSpectrum (𝓞 ℚ)` associated to a prime number. )) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    1 +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. ↑pℕ
    A 3-adic hardly ramified representation has trace(Frob_p) = 1 + p for all p ≠ 2,3
    contains sorry in proof
Proof

This theorem is formalized in Lean under the attached declaration.

Theorem hardly_ramified_reducible (if \ell\geq 3 is a prime and \overline{\rho}:\GQ\to\GL_2(\Z/\ell\Z) is hardly ramified, then \overline{\rho} is reducible) is an easy consequence of these theorems, as we now show.

Proof

Theorem 3.5 Theorem 3.6 Theorem 3.8 Assume for a contradiction that \overline{\rho} is irreducible. By theorem hardly_ramified_lifts, \overline{\rho} lifts to a hardly ramified \ell-adic representation \rho. By theorem hardly_ramified_spreads_out, \rho is part of a compatible family of q-adic Galois representations. By theorem hardly_ramified_3adic_reducible, any 3-adic member \rho_3 of this family has semisimplification 1\oplus\chi_3 and in particular for p\nmid 6 we have that the characteristic polynomial of \rho_3(\Frob_p) is (X-p)(X-1). By compatibility of the family we deduce that for p\nmid 6\ell the characteristic polynomial of \rho(\Frob_p) is (X-p)(X-1), and thus the characteristic polynomial of \overline{\rho}(\Frob_p) is (X-p)(X-1). By the Chebotarev density theorem, \overline{\rho} and 1\oplus\chi have the same characteristic polynomials everywhere (here \chi is the mod \ell cyclotomic character). Thus by the Brauer-Nesbitt theorem, \overline{\rho} is reducible, the contradiction we seek.

What remains then, modulo several results which were known in the 1980s, is to prove the three theorems hardly_ramified_lifts, hardly_ramified_spreads_out, and hardly_ramified_3adic_reducible. By far the easiest is theorem hardly_ramified_3adic_reducible; this follows from old estimates of Fontaine, ultimately relying on bounds for root discriminants due to Odlyzko and Poitou, originally developed to prove that there was no nontrivial abelian scheme over \mathbf{Z}. The other two theorems are deeper, and both use modern variants of Wiles' R = T machinery.

We have not yet written any more LaTeX on how to proceed further; the rest of this blueprint should be considered as more unfocussed thoughts.