General Semilinear group

Stream: mathlib4

[Edward van de Meent]

i'd like to prove a variant of docs#LinearEquiv.automorphismGroup where semilinear equivalences with automorphisms on R are also considered...
My current approach uses Sigma to describe the space as (σ:RingAut R) × (@LinearEquiv R R _ _ (σ) (σ.symm) (RingHomInvPair.of_ringEquiv σ) (RingHomInvPair.of_ringEquiv σ).symm) M M (lean needs some help to realise that ringauts have inverses and the like)

i am almost done, but i am having trouble closing one last goal...

Code

import Mathlib.Algebra.Module.Equiv

abbrev SemilinearAut (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M]: Type _ :=
    (σ:RingAut R) × (@LinearEquiv R R _ _ (σ) (σ.symm)
      (RingHomInvPair.of_ringEquiv σ)
      (RingHomInvPair.of_ringEquiv σ).symm) M M

instance {R M :Type*} [a:Semiring R] [b:AddCommMonoid M] [c:Module R M]: Group (SemilinearAut R M) where
  mul := fun ⟨σ₁,f₁⟩ ⟨σ₂,f₂⟩ => ⟨σ₂.trans σ₁, (@LinearEquiv.trans R R R M M M a a a b b b
    c c c σ₂ σ₁ (σ₂.trans σ₁) σ₂.symm σ₁.symm (σ₂.trans σ₁).symm ⟨by exact RingEquiv.coe_ringHom_trans σ₂ σ₁⟩ ⟨by exact rfl⟩
    (RingHomInvPair.of_ringEquiv σ₂) (RingHomInvPair.of_ringEquiv σ₁)
    (RingHomInvPair.of_ringEquiv (σ₂.trans σ₁))
    (RingHomInvPair.of_ringEquiv σ₂).symm (RingHomInvPair.of_ringEquiv σ₁).symm
    (RingHomInvPair.of_ringEquiv (σ₂.trans σ₁)).symm
    ) f₂ f₁⟩
  mul_assoc := fun ⟨σ₁,f₁⟩ ⟨σ₂,f₂⟩ ⟨σ₃,f₃⟩ => by
    simp_rw [HMul.hMul]
    simp only [RingEquiv.coe_ringHom_trans, Sigma.mk.inj_iff, heq_eq_eq]
    constructor <;> rfl
  one := ⟨RingEquiv.refl R, LinearEquiv.refl R M⟩
  one_mul := fun a => by
    simp_rw [HMul.hMul,OfNat.ofNat]
    simp only [RingEquiv.coe_ringHom_trans, LinearEquiv.trans_refl]
    rfl
  mul_one := fun a => by
    simp_rw [HMul.hMul,OfNat.ofNat]
    simp only [RingEquiv.coe_ringHom_trans, LinearEquiv.refl_trans]
    rfl
  inv := fun ⟨σ,f⟩ => ⟨σ.symm,f.symm⟩
  mul_left_inv := fun ⟨σ,f⟩ => by
    simp only [RingEquiv.coe_ringHom_trans]
    simp_rw [HMul.hMul,OfNat.ofNat]
    simp only [RingEquiv.coe_ringHom_trans, Sigma.mk.inj_iff, RingEquiv.self_trans_symm,
      RingEquiv.coe_ringHom_refl, RingEquiv.symm_refl, true_and]
    sorry

[Edward van de Meent]

something that would possibly help is being able to simp only at the type of a subexpression of the goal... does something like that exist?

[Eric Wieser]

The abbrev can be simplified slightly to:

abbrev SemilinearAut (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M]: Type _ :=
    (σ:RingAut R) × (letI inst := RingHomInvPair.of_ringEquiv σ; letI := inst.symm; M ≃ₛₗ[(σ : R →+* R)] M)

(which is really exactly the same thing)

[Eric Wieser]

I recommend taking a step back and first writing an ext lemma that says when two SemilinearAuts are equal

[Eric Wieser]

Namely; "the RingAut parts are equal, and the linear maps, when treated as additive maps, are equal

[Edward van de Meent]

Eric Wieser said:

Namely; "the RingAut parts are equal, and the linear maps, when treated as additive maps, are equal

i run into a similar problem, where i have to prove HEq snd✝¹ snd✝, with the types snd✝¹: M ≃ₛₗ[↑fst✝¹] M and snd✝:M ≃ₛₗ[↑fst✝] M, when i have h₁: fst✝¹ = fst✝ and h₂: ∀ (x : M), snd✝¹ x = snd✝ x. i'd like to rewrite with h₁ in the type of snd✝¹ so i can apply heq_eq_eq and then something like funext...

protected lemma SemilinearAut.ext {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
  ⦃f g: SemilinearAut R M⦄ (h₁: f.fst = g.fst) (h₂: ∀ (x: M), f.snd x = g.snd x): f = g := by
  cases f; cases g; congr
  simp_all? says simp_all only
  sorry

[Eric Wieser]

This works for me:

protected lemma SemilinearAut.ext {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
  ⦃f g: SemilinearAut R M⦄ (h₁: f.1 = g.1) (h₂: ∀ (x: M), f.2 x = g.2 x): f = g := by
  cases f; cases g
  subst h₁
  congr
  ext x
  exact h₂ _

[Eric Wieser]

Your congr was too early; you want to try and eliminate the dependent types before you split componentwise

[Edward van de Meent]

thanks!

[Edward van de Meent]

i also just found heq_of_eqRec_eq : ∀ {α β : Sort u} {a : α} {b : β} (h₁ : α = β), h₁ ▸ a = b → HEq a b...

[Eric Wieser]

Now, the trick I'd use to prove this group structure is first show that there is an injection to RingAut \times AddAut, define mul/one/inv as you've done, then pull back the group structure through docs#Function.Injective.group

[Edward van de Meent]

does it happen to be the case that for a semilinear equivalence, the choice of RingEquivalence is forced? i did some thinking, and this is true if the action of R on M (with Module R M) is faithful... is this always the case, or not? i've tried thinking of a counterexample with Module Z (Z/n) but there i run into the problem that there is a unique RingEquiv on Z...

[Edward van de Meent]

another way of asking the same thing is "is the (canonical) mapping from semilinear equivalence to addhom injective?"

[Johan Commelin]

Let A be the ring of polynomials over your favourite base ring R. Let M be an R-module. View M as an A-module by letting every polynomial act via its constant coefficient. (In other words, X acts as multiplication by 0.)
Let f be an R-linear endomorphism of M. Then f is also A-semilinear wrt any R-algebra endomorphism of A.

[Edward van de Meent]

i'm not very familiar with algebras, could you give a specific example of two different R-algebra endomorphisms of A?

[Edward van de Meent]

i suppose X ↦ u X with u a non-1 unit might do....

[Edward van de Meent]

(along with identity)

[Johan Commelin]

An R-algebra hom out of A is determined by the image of X. And you can send X wherever you want.

[Edward van de Meent]

surely it has to be bijective though?

[Johan Commelin]

Why?

[Edward van de Meent]

because i'm looking at linear equivalences

[Johan Commelin]

Ooh, ok. Well you can send X to a * X + b with a invertible.

[Edward van de Meent]

right, thanks :+1:

[Adam Topaz]

Re the title: it’s sometimes called the “general semilinear group”

[Edward van de Meent]

i'm thinking a bit, the typical consideration of "general semilinear group" might not quite be the same as the group structure on SemilinearAut R M := (σ:RingAut R) × (M ≃ₛₗ[(σ : R →+* R)] M), as there in the second, there can be multiple copies of the same function, if there are multiple fitting ringEquivs...

[Edward van de Meent]

however, i can imagine that the typical consideration doesnt...

[Adam Topaz]

Well, for one it should be the semi direct product. Also, this will indeed only agree with the set of semiliear equivs under some faithfulness assumptions

[Edward van de Meent]

how do you mean semidirect product?

[Edward van de Meent]

in the group sense?

[Adam Topaz]

Oh you write the semilinear equivs. Sorry, you’re correct. What I meant is if you take the product with the linear equivs, then you need to take a semi direct product

[Adam Topaz]

In the group sense

[Adam Topaz]

(Sorry, I’m doing this on my phone)

[Edward van de Meent]

would it be possible to get the "smaller" group by looking at some quotient, perhaps?

[Adam Topaz]

I guess you could identify two terms in the sigma type you wrote down is the induced function on the module is the same.

[Adam Topaz]

At least for such a quotient you would get an extensionality principle based on the underlying function

[Adam Topaz]

And in the case where the action is faithful, the two variants should agree

[Edward van de Meent]

right... i suppose that that would be the quotient with the subgroup of the identity map with all its possible ringisomorphisms?

[Adam Topaz]

I was actually envisioning doing something like this:

import Mathlib

variable (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M]

-- Why doesn't this exist?
instance (σ : R ≃+* R) :  RingHomInvPair (σ : R →+* R) σ.symm where
  comp_eq := σ.symm_comp
  comp_eq₂ := σ.comp_symm

instance (σ τ : R ≃+* R) : RingHomCompTriple (σ : R →+* R) (τ : R →+* R)
      (σ.trans τ : R →+* R) where
    comp_eq := rfl

def GSL := (σ : R ≃+* R) × (M ≃ₛₗ[(σ : R →+* R)] M)

instance : CoeFun (GSL R M) (fun _ => M → M) where
  coe f := f.snd

def GSLSetoid : Setoid (GSL R M) := Setoid.ker fun f => (f : M → M)

def GSL' := Quotient (GSLSetoid R M)

[Edward van de Meent]

in case you didn't know about it: docs#RingHomInvPair.of_ringEquiv

[Adam Topaz]

Ok great! I didnt check too carefully :)

[Edward van de Meent]

but it isn't an instance probably for loop reasons...

[Edward van de Meent]

right... defining the group instance afterward might be a bit annoying though, because it is a quotient type. i'd rather use docs#QuotientGroup.Quotient.group

[Adam Topaz]

I disagree. Since you’re just identifying two terms if they have the same underlying functions, and composition should be obviously compatible with function composition, defining the group structure using Quotient.lift should be trivial

[Adam Topaz]

And the setoid used for quotient groups won’t be as convenient to work with definitionally

[Edward van de Meent]

i hadn't thought of that...

[Edward van de Meent]

maybe the best of both worlds is lifting the group structure from AddAut?

[Edward van de Meent]

because the map from (σ : R ≃+* R) × (M ≃ₛₗ[(σ : R →+* R)] M) to AddAut M is a grouphom

[Adam Topaz]

Oh yes that’s probably the way to go

[Edward van de Meent]

something that i do keep walking into right now is that the api for using ring-isos with semilinear equivalences is quite poor... simp lemmas hardly ever apply.

[Adam Topaz]

Edward van de Meent said:

something that i do keep walking into right now is that the api for using ring-isos with semilinear equivalences is quite poor... simp lemmas hardly ever apply.

That’s not good… do you have a #mwe illustrating such a failure?

[Edward van de Meent]

i tried, it turns out the lack of API is with my own classes rather than with Matlib :upside_down: