More GaloisRep API

Stream: FLT

[Stepan Nesterov]

Are any of these theorems equivalent to results in mathlib?

theorem reducible_base_change_of_reducible {K E F : Type*} [Field K] [Field E] [Field F]
  [TopologicalSpace E] [IsTopologicalRing E] [TopologicalSpace F] [IsTopologicalRing F]
  [Algebra E F] {V : Type*} [AddCommGroup V] [Module E V] [Module.Finite E V] [ContinuousSMul E F]
  (ρ : GaloisRep K E V) : ¬GaloisRep.IsIrreducible ρ →
    ¬GaloisRep.IsIrreducible (GaloisRep.baseChange F ρ) := sorry

theorem reducible_conj_reducible_iff {K R : Type*} [Field K] [TopologicalSpace R] [Field R]
  [IsTopologicalRing R] {V W : Type*} [AddCommGroup V] [Module R V] [Module.Finite R V]
  [AddCommGroup W] [Module R W] [Module.Finite R W] [Module.Free R W]
  (ρ : GaloisRep K R V) (e : V ≃ₗ[R] W) : GaloisRep.IsIrreducible ρ ↔
  GaloisRep.IsIrreducible (GaloisRep.conj ρ e) := sorry

def tensor_associator {R : Type*} (S T : Type*) [CommRing R] [CommRing S] [CommRing T] [Algebra R S]
  [Algebra S T] [Algebra R T] [IsScalarTower R S T] (V : Type*) [AddCommGroup V] [Module R V] :
  TensorProduct R T V ≃ₗ[T] TensorProduct S T (TensorProduct R S V) := by exact
    (TensorProduct.AlgebraTensorModule.cancelBaseChange R S T T V).symm

theorem base_change_trans {K R : Type} (S T : Type*) [Field K] [TopologicalSpace R] [CommRing R]
  [IsTopologicalRing R] [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [TopologicalSpace T]
  [CommRing T] [IsTopologicalRing T] [Algebra R S] [ContinuousSMul R S] [Algebra S T] [Algebra R T]
  [ContinuousSMul S T] [IsScalarTower R S T] [ContinuousSMul R T]
  {V : Type*} [AddCommGroup V] [Module R V] [Module.Finite R V] [Module.Free R V]
  (ρ : GaloisRep K R V) : GaloisRep.conj (GaloisRep.baseChange T ρ) (tensor_associator S T V) =
  (GaloisRep.baseChange T (GaloisRep.baseChange S ρ)) := sorry

I have no idea how to search for something like this

[Chris Birkbeck]

You can try searching using Loogle

[Kenny Lau]

mathlib also prefers "constructive" statements, i.e. your first statement should say q -> p instead of not p -> not q

[Kenny Lau]

and for the third one you answered your own question

[Kevin Buzzard]

For the first one, GaloisRep.IsIrreducible is defined in terms of Representation.IsIrreducible which is in FLT not Mathlib (shockingly) and there is no API for it. Also GaloisRep.baseChange is not defined in terms of any mathlib baseChange and there's essentially no API for it. So here the most helpful thing to do would be to first upstream Subrepresentation (the contents of FLT/Deformations/RepresentationTheory/Subrepresentation.lean) and then Irreducible (the contents of FLT/Deformations/RepresentationTheory/Irreducible.lean) to mathlib (we are super-weak on representation theory because it took forever to finish the discussion about what the definition of Representation should be), then define baseChange on both Representation and Subrepresentation (follow how Andrew did it for GaloisRep for Representation although it's easier because you don't have to worry about continuity), prove ¬IsIrreducible ρ implies the existence of a nontrivial sub, prove that under certain conditions nontrivial subs base change to nontrivial subs (exercise: in what generality is this true? Base change will presumably work for any morphism of commutative semirings but reduction mod p won't in general preserve reducibility), and deduce the result from that.

The cop-out if you just want to proceed is to define base change on Representation and Subrepresentation in FLT and go on from there. But this stuff should definitely all be in Mathlib.

[Kevin Buzzard]

For the second one, again this should be deducible from a bare theorem about Representations, but we don't have Representation.conj again because Mathlib is weak on representation theory right now. In fact one of the reasons I am motivated to do a project like FLT is that projects like this expose weaknesses in Mathlib, and this is what is happening here. One can look at the API Andrew wrote for GaloisRep.conj and this informs what the API for Representation.conj should be. One thing which isn't there as far as I can see is the lattice bijection between Subrepresentation X and Subrepresentation Y if X and Y are isomorphic representations, so that's another thing which should go in mathlib's Subrepresentation API.

[Kevin Buzzard]

tensor_associator (which you're not asking about) would usually be stated as T ⊗[R] V ≃ₗ[T] T ⊗[S] (S ⊗[R] V) and, in stark contrast to representations, we have an absolute ton of stuff on tensor products, so here of course you're OK. Note that as a general rule in mathlib we put the more complex thing on the LHS of the equality/isomorphism, which is why you had to use .symm. And the third sorry is one of those things which hopefully the system has enough to do relatively easily...yeah, here's a proof

theorem base_change_trans {K R : Type} (S T : Type*) [Field K] [TopologicalSpace R] [CommRing R]
    [IsTopologicalRing R] [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
    [TopologicalSpace T] [CommRing T] [IsTopologicalRing T] [Algebra R S] [ContinuousSMul R S]
    [Algebra S T] [Algebra R T] [ContinuousSMul S T] [IsScalarTower R S T] [ContinuousSMul R T]
    {V : Type*} [AddCommGroup V] [Module R V] [Module.Finite R V] [Module.Free R V]
    (ρ : GaloisRep K R V) : GaloisRep.conj (GaloisRep.baseChange T ρ) (tensor_associator S T V) =
    (GaloisRep.baseChange T (GaloisRep.baseChange S ρ)) := by
  ext g v
  simp
  exact?

(note: indent 4 before the :=)

[Yaël Dillies]

Kevin Buzzard said:

Note that as a general rule in mathlib we put the more complex thing on the LHS of the equality/isomorphism

In fact, this rule only holds for equalities, and instead the inverse rule usually holds for isomorphisms. This is because equalities get rewritten while isomorphisms get applied, and rewriting is more or less the same thing as applying backwards.

[Kevin Buzzard]

Go tell that to docs#TensorProduct.AlgebraTensorModule.cancelBaseChange . More generally, Is this true in tensor product world?

[Yaël Dillies]

My "usually" above is load-bearing. I am sure different parts of mathlib have different subconventions. I simply wanted to point out that the usual rule for equalities really does not translate to an agreed-upon convention for isomorphisms

[Bryan Wang]

Subrepresentation is upstreamed in #31554