Definition of absolute irreducibility

Stream: FLT

[Stepan Nesterov]

Currently absolute irreducibility is defined in FLT by

class IsAbsolutelyIrreducible : Prop where
  absolutelyIrreducible : ∀ k', ∀ _ : Field k', ∀ _ : Algebra k k', IsIrreducible (k' ⊗ᵣ' ρ)

Then, if you try to prove that an absolutely irreducible representation is irreducible:

theorem isIrreducible_of_isAbsoultelyIrreducible (h : IsAbsolutelyIrreducible ρ) :
    IsIrreducible ρ := by
  obtain ⟨h⟩ := h
  specialize h k (by assumption) (by infer_instance)
  sorry

you need to work with (k⊗ᵣ'ρ), which is a Representation k G (TensorProduct k k W), and it seems like it would be quite painful to manually go between (TensorProduct k k W) and W every single time.
This reminds me of old blogpost by Kevin, where he explains that in a definition of a structure sheaf of an affine scheme, you do not use localizations defined by an explicit construction, but an arbitrary localization defined by a universal property. Can we do something similar here?
Is there a representation API with which I can say "A $K$-linear representation $\rho$ is absolutely irreducible, if for any field extension $K'/K$, and for any $K'$-linear representation, which satisfies the universal property of base change of $\rho$ to $K'$, that representation is irreducible"?

[Scott Carnahan]

Are you asking for a Prop-valued IsBaseChange class?

[Thomas Browning]

Presumably, the actual definition of IsAbsolutelyIrreducible can remain more concrete, but there should be API saying that every IsBaseChange is irreducible.

[Thomas Browning]

Also, is it sufficient to ask for irreducibility over the algebraic closure? Because that would avoid the quantification over types.

[Stepan Nesterov]

Thomas Browning said:

Also, is it sufficient to ask for irreducibility over the algebraic closure? Because that would avoid the quantification over types.

It is equivalent to just irreducibility over the algebraic closure, and I’m trying to prove that as a theorem. I also replaced locally in my file Field with Field.{u}, so that it’s quantifying over the fields in the same universe as k only.

[Kevin Buzzard]

I can't imagine that the definition is used anywhere right now other than to state theorems, so I'd be happy to change it.