Set.matrix

Stream: Is there code for X?

[Kevin Buzzard]

We have docs#Set.prod which enables me to take the product of two subsets as a subset of the product. But we don't seem to have

import Mathlib

def Set.matrix {X : Type*} {ι₁ ι₂ : Type*} (S : Set X) :
    Set (Matrix ι₁ ι₂ X) := {m | ∀ i j, m i j ∈ S}

(is that the way to spell it?). Or did I miss it?

My set-up is that I have a topological ring $K$ (e.g. the p-adic numbers) and a compact open subring $R$ (e.g. the p-adic integers, of type Subring K) and I want to (idiomatically) say things like "$M_2(R)$ is a compact open subring of $M_2(K)$" but right now I'm not sure I can even build the subring from what we have. I am envisaging something like this:

import Mathlib

def Set.matrix {X : Type*} (ι₁ ι₂ : Type*) (S : Set X) :
    Set (Matrix ι₁ ι₂ X) := {m | ∀ i j, m i j ∈ S}

def Setlike.matrix {X : Type*} (ι₁ ι₂ : Type*) {T : Type*} [SetLike T X] (S : T) :
    Set (Matrix ι₁ ι₂ X) := {m | ∀ i j, m i j ∈ S}

def AddSubmonoidClass.matrix {A : Type*} [AddMonoid A] (ι₁ ι₂ : Type*)
    {T : Type*} [SetLike T A] [AddSubmonoidClass T A] (S : T) :
    AddSubmonoid (Matrix ι₁ ι₂ A) where
      carrier := Set.matrix _ _ S
      add_mem' hm hn i j := add_mem (hm i j) (hn i j)
      zero_mem' _ _ := zero_mem _

def AddSubgroupClass.matrix {A : Type*} [AddGroup A] (ι₁ ι₂ : Type*)
    {T : Type*} [SetLike T A] [AddSubgroupClass T A] (S : T) :
    AddSubgroup (Matrix ι₁ ι₂ A) where
      __ := AddSubmonoidClass.matrix _ _ S
      neg_mem' hm i j := neg_mem (hm i j)

def SubringClass.matrix {X : Type*} [Ring X] (ι : Type*) [Fintype ι] [DecidableEq ι]
    {T : Type*} [SetLike T X] [SubringClass T X] (S : T) :
    Subring (Matrix ι ι X) where
      __ := AddSubgroupClass.matrix ι ι S
      mul_mem' ha hb := sorry
      one_mem' := sorry

def Set.matrix_isOpen {X : Type*} [TopologicalSpace X] {ι₁ ι₂ : Type*} [Fintype ι₁]
    [Fintype ι₂] {S : Set X} (hS : IsOpen S) :
    IsOpen (S.matrix ι₁ ι₂) := by
  rw [isOpen_pi_iff']
  intro f hf
  use fun i ↦ {g | ∀ j, g j ∈ S}
  refine ⟨fun i ↦ ⟨?_, hf i⟩, fun f hf ↦ by simpa using hf⟩
  rw [isOpen_pi_iff']
  intro g hg
  use fun j ↦ S
  exact ⟨fun j ↦ ⟨hS, hg j⟩, fun g hg ↦ by simp_all⟩

Does this sound like a sensible way to do things?

[Kenny Lau]

the last def is a theorem; don't you have a different topology than the product topology?

[Eric Wieser]

I think the use of Classes here is a bad idea, and you should just write these for the direct subobjects

[Kevin Buzzard]

Aha, because it's not that difficult in practice to turn a subring into an additive subgroup

[Eric Wieser]

Yeah, and if you don't force the user to do it when using the definition, they're going to suffer with the theorems instead

[Bryan Wang]

I just found out there is Ideal.matricesOver which is basically the same thing but for ideals of rings instead of subrings of rings; would it make sense then to place the above in something like Mathlib.LinearAlgebra.Matrix.Subring and have Subring.matricesOver?

[Kevin Buzzard]

That looks like an odd naming convention to me. Do we have Over anywhere else? On the other hand if it's there already should we stick with it?

[Bryan Wang]

Very different meaning of the word 'over', but I can only think of Ideal.primesOver that's similar

[Bryan Wang]

But yeah matricesOver is used pretty heavily in Mathlib.LinearAlgebra.Matrix.Ideal, so I'm slightly inclined to stick with it

[Kevin Buzzard]

I really want to stress that I think "matricesOver" stinks has a name. It doesn't matter how heavily it's used, we have search/replace. I think Subring.matrix and Ideal.matrix are both immediately guessable, and independent of that I cannot imagine how we let "matrices" in when everything else is "matrix".

[Kevin Buzzard]

Oh I tell a lie there is also docs#pairSelfAdjointMatricesSubmodule

I am in two minds about whether to argue for Subring.matrix or Subring.matricesOver. Having said that, if Ideal.matricesOver didn't exist yet then I am 100% sure what I would be arguing for :-)

[Eric Wieser]

I agree that .matrix is clearly better than .matricesOver, as it matches docs#Submodule.pi etc

[Eric Wieser]

I think what probably happens is that someone notices the bad name in a PR using matricesOver, then gets told "I agree, but renaming it is out of scope" (which is true), and then neither the reviewer or the contributor follow up by trying to snipe someone on Zulip to do the rename.

[Kevin Buzzard]

@Bryan Wang why don't you make a PR defining AddSubgroup.matrix, Subring.matrix etc on the basis that it conforms with most of the mathlib naming convention (e.g. docs#AddSubgroup.prod , docs#AddSubgroup.pi etc) and then if you really want to be heroic you could (in another PR!) attempt the refactor of .matricesOver to .matrix, although I suspect that right now this will involve a lot of manual deprecations.

[Bryan Wang]

Sure! Yeah .matrix is for sure the better name if .matricesOver didn't exist

[Eric Wieser]

Now that we have docs#Set.matrix I guess it's time to deprecate docs#Ideal.matricesOver

[Bryan Wang]

yep, I can take care of that sometime this week!

[Bryan Wang]

Eric Wieser said:

Now that we have docs#Set.matrix I guess it's time to deprecate docs#Ideal.matricesOver

this is #27575!