Subring.closure_induction proof

Stream: Is there code for X?

[Edison Xie]

Is there a quicker (shorter) proof than this? Thanks in advance!

import Mathlib

example (K D : Type*) [Field K] [DivisionRing D] [Algebra K D]
    (L : Subalgebra K D) (L_comm : ∀ x ∈ L, ∀ y ∈ L, x * y = y * x) (a x y : D)
    (hx : x ∈ Subring.closure (insert a (Set.range ⇑(algebraMap K D) ∪ ↑L)))
    (hy : y ∈ Subring.closure (insert a (Set.range ⇑(algebraMap K D) ∪ ↑L))) (ha : ∀ g ∈ L, g * a = a * g) (x1 y1 : D)
    (hx1 : x1 ∈ insert a (Set.range ⇑(algebraMap K D) ∪ ↑L)) (hy1 : y1 ∈ insert a (Set.range ⇑(algebraMap K D) ∪ ↑L)) :
  x1 * y1 = y1 * x1 := by
    simp at hx1 hy1
    obtain hx11 | hx12 | hx13 := hx1
    all_goals obtain hy11 | hy12 | hy13 := hy1
    · simp_all
    · obtain ⟨b, rfl⟩ := hy12
      exact Algebra.commutes _ _ |>.symm
    · subst hx11
      exact ha _ hy13|>.symm
    · obtain ⟨b, rfl⟩ := hx12
      exact Algebra.commutes _ _
    · obtain ⟨b, rfl⟩ := hx12
      exact Algebra.commutes _ _
    · obtain ⟨b, rfl⟩ := hx12
      exact Algebra.commutes _ _
    · subst hy11
      exact ha _ hx13
    · obtain ⟨b, rfl⟩ := hy12
      exact Algebra.commutes _ _ |>.symm
    · exact L_comm x1 hx13 y1 hy13

[Edison Xie]

Or equivalently, is there a shorter proof to prove this? Subalgebra.adjoin_induction2 doesn't seem to work...

import Mathlib

lemma SubField.adjoin_centralizer_mul_comm (K D : Type*) [Field K] [DivisionRing D] [Algebra K D]
    (L : Subalgebra K D) (a : D) (ha : a ∈ Subalgebra.centralizer K L)
    (L_comm : ∀ x ∈ L, ∀ y ∈ L, x * y = y * x): ∀ (x y : D), x ∈ Algebra.adjoin K (L ∪ {a}) →
    y ∈ Algebra.adjoin K (L ∪ {a}) → x * y = y * x :=
  fun x y hx hy ↦ by
    simp only [Set.union_singleton, Algebra.mem_adjoin_iff, Set.union_insert,
      Subalgebra.mem_centralizer_iff, SetLike.mem_coe] at hx hy ha
    refine Subring.closure_induction₂ (R := D) (fun x1 y1 hx1 hy1 ↦ by
      simp only [Set.mem_insert_iff, Set.mem_union, Set.mem_range, SetLike.mem_coe] at hx1 hy1
      obtain hx11 | hx12 | hx13 := hx1
      all_goals obtain hy11 | hy12 | hy13 := hy1
      · simp_all
      · obtain ⟨b, rfl⟩ := hy12
        exact Algebra.commutes _ _ |>.symm
      · subst hx11
        exact ha _ hy13|>.symm
      · obtain ⟨b, rfl⟩ := hx12
        exact Algebra.commutes _ _
      · obtain ⟨b, rfl⟩ := hx12
        exact Algebra.commutes _ _
      · obtain ⟨b, rfl⟩ := hx12
        exact Algebra.commutes _ _
      · subst hy11
        exact ha _ hx13
      · obtain ⟨b, rfl⟩ := hy12
        exact Algebra.commutes _ _ |>.symm
      · exact L_comm x1 hx13 y1 hy13) ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ hx hy
    all_goals try simp_all [add_mul, mul_add]
    · rintro x y z - - - hxz hyz
      rw [mul_assoc, hyz, ← mul_assoc, hxz, mul_assoc]
    · rintro x y z - - - hxy hxz
      rw [← mul_assoc, hxy, mul_assoc, hxz, ← mul_assoc]

[Kenny Lau]

@Edison Xie

import Mathlib

open Set

lemma SubField.adjoin_centralizer_mul_comm (K D : Type*) [Field K] [DivisionRing D] [Algebra K D]
    (L : Subalgebra K D) (a : D) (ha : a ∈ Subalgebra.centralizer K L)
    (L_comm : ∀ x ∈ L, ∀ y ∈ L, x * y = y * x): ∀ (x y : D), x ∈ Algebra.adjoin K (L ∪ {a}) →
    y ∈ Algebra.adjoin K (L ∪ {a}) → x * y = y * x :=
  fun x y hx hy ↦ by
    refine (fun h₃ ↦ Algebra.adjoin_induction₂ ?_ ?_ h₃ ?_ ?_ ?_ ?_ ?_ hx hy) ?_
    · intro r x hx; exact Or.elim hx (fun hx ↦ (L_comm x hx _ (algebraMap_mem ..)).symm)
        (fun _ ↦ by convert ha _ (algebraMap_mem ..))
    · exact fun x y hx hy ↦ Or.elim hx
        (fun hx ↦ Or.elim hy (L_comm x hx y) (fun _ ↦ by convert ha x hx))
        fun hx ↦ Or.elim hy (fun hy ↦ by convert (ha y hy).symm) (fun hy ↦ by rw [hx, hy])
    · intros r₁ r₂; rw [← map_mul, ← map_mul, mul_comm]
    · intro r x hx; rw [h₃ r x hx]
    · intros; simp only [add_mul, mul_add, *]
    · intros; simp only [add_mul, mul_add, *]
    · intros _ _ _ _ _ _ hxz hyz; rw [mul_assoc, hyz, ← mul_assoc, hxz, mul_assoc]
    · intros _ _ _ _ _ _ hxy hxz; rw [← mul_assoc, hxy, mul_assoc, hxz, mul_assoc]

[Kenny Lau]

I used Algebra.adjoin_induction₂ and a clever trick to re-use a proof in two goals

[Kenny Lau]

but actually I think I would split this into two lemmas

[Kenny Lau]

aha, i tried to split into two lemmas but failed: Algebra ↥L D is not true!

[Kenny Lau]

so yeah there's no way to write it as Algebra.adjoin L {a} it seems...
(there is a way to do it, but now it doesn't feel like it's worth the effort, because you're proving this theorem regardless)

[Eric Wieser]

Is this true more generally for any two commutative subalgebras whose elements also commute?

[Kenny Lau]

it would seem so

[Kenny Lau]

well it doesn't seem to be exactly more general, crucially here {a} is not a subalgebra, and we get commutativity on {a} for free

[Kenny Lau]

so maybe a more general statement could be... Algebra R A, s t : Set A, then Algebra.adjoin R (s ∪ t) is commutative if s is commutative, t is commutative, and s commutes with t

[Kenny Lau]

indeed actually the generalisation we might want, is "is commutative" as a property of subalgebras

[Kenny Lau]

import Mathlib

namespace Subalgebra

def IsComm {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : Prop :=
  ∀ x ∈ S, ∀ y ∈ S, x * y = y * x

variable {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]

theorem IsComm.bot : IsComm (⊥ : Subalgebra R A) := by
  refine fun x hx y hy ↦ ?_
  rw [Algebra.mem_bot, Set.mem_range] at hx hy
  rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
  rw [← map_mul, ← map_mul, mul_comm]

end Subalgebra

[Edison Xie]

Eric Wieser said:

Is this true more generally for any two commutative subalgebras whose elements also commute?

note that the centralizer of L need not to be commutative

[Kenny Lau]

does anyone want to adopt IsComm as a PR? :melt:

[Kenny Lau]

it's a bit hard to adopt things now because branches have to be personal...

[Andrew Yang]

We have docs#IsMulCommutative

[Eric Wieser]

Edison Xie said:

note that the centralizer of L need not to be commutative

Don't you only care that Algebra.adjoin K {a} is commutative?

[Eric Wieser]

The statement I have in mind is

lemma Subalgebra.isComm_sup {R A} [CommSemiring R] [Semiring A] [Algebra R A]
    (S₁ S₂ : Subalgebra R A) (h₁ : IsMulCommutative S₁) (h₂ : IsMulCommutative S₁)
    (h₁₂ : ∀ x₁ ∈ S₁, ∀ x₂ ∈ S₂, Commute x₁ x₂) :
    IsMulCommutative ↥(S₁ ⊔ S₂) :=
  sorry

[Eric Wieser]

(deleted)

[Eric Wieser]

lemma Subalgebra.isComm_sup {ι R A} [CommSemiring R] [Semiring A] [Algebra R A]
    (S : ι → Subalgebra R A) (h₁ : ∀ i, IsMulCommutative (S i))
    (h₁₂ : Pairwise fun i j => ∀ x₁ ∈ S i, ∀ x₂ ∈ S j, Commute x₁ x₂) :
    IsMulCommutative ↥(⨆ i, S i) := by
  constructor
  constructor
  rintro ⟨x, hx⟩ ⟨y, hy⟩
  ext
  show Commute x y
  induction hx using Algebra.iSup_induction' with
  | zero => exact .zero_left _
  | one => exact .one_left _
  | add x₁ x₂ hx hx₂ ihx₁ ihx₂ => exact ihx₁.add_left ihx₂
  | mul x₁ x₂ hx hx₂ ihx₁ ihx₂ => exact ihx₁.mul_left ihx₂
  | algebraMap r => exact Algebra.commutes _ _
  | basic i x hx =>
  induction hy using Algebra.iSup_induction' with
  | zero => exact .zero_right _
  | one => exact .one_right _
  | add x₁ x₂ hx hx₂ ihx₁ ihx₂ => exact ihx₁.add_right ihx₂
  | mul x₁ x₂ hx hx₂ ihx₁ ihx₂ => exact ihx₁.mul_right ihx₂
  | algebraMap r => exact (Algebra.commutes _ _).symm
  | basic j y hy =>
  obtain rfl | hij := eq_or_ne i j
  · exact congrArg Subtype.val <| h₁ _ |>.is_comm.comm ⟨x, hx⟩ ⟨y, hy⟩
  · exact h₁₂ hij _ hx _ hy

[Eric Wieser]

I think there's some machinery around docs#IsMulCommutative that could improve here

[Eric Wieser]

@loogle IsMulCommutative, Commute

[loogle]

:shrug: nothing found

[Jireh Loreaux]

I think you should be able to get all this from docs#Subalgebra.centralizer_coe_sup and the fact that a subalgebra is commutative iff its contained in it's centralizer.

[Jireh Loreaux]

@Eric Wieser I'd prefer not to spell things in terms of IsMulCommutative unless we need to. In this case, I think there is a bit of missing API for Subalgebra.centralizer and a few other things, but once you use the correct spelling, it's quite natural. @Edison Xie or @Kenny Lau, you might be interested in this also. Note the original request appears in the bottom two lemmas.

import Mathlib.Algebra.Algebra.Subalgebra.Centralizer

open Algebra Subalgebra

-- this is the heart of the result you want.
lemma Subalgebra.sup_le_centralizer_self {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
    {S₁ S₂ : Subalgebra R A} (h₁ : S₁ ≤ centralizer R S₁) (h₂ : S₂ ≤ centralizer R S₂)
    (h₁₂ : S₁ ≤ centralizer R S₂) :
    (S₁ ⊔ S₂) ≤ centralizer R ↑(S₁ ⊔ S₂) := by
  simpa [centralizer_coe_sup, sup_le_iff, le_inf_iff, h₁, h₂, le_centralizer_iff (S := S₂)] using h₁₂

-- Maybe this should be about `S : Subalgebra R A` and `T : Set A` instead? I'm not sure.
lemma Subalgebra.le_centralizer_iff_commute {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
    (S T : Subalgebra R A) :
    S ≤ centralizer R T ↔ ∀ y ∈ S, ∀ x ∈ T, Commute x y := by
  rfl

lemma Subalgebra.centralizer_adjoin {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
    (s : Set A) : centralizer R (adjoin R s) = centralizer R s := by
  apply le_antisymm (centralizer_le _ _ _ subset_adjoin)
  intro z hz
  simp only [mem_centralizer_iff, SetLike.mem_coe] at hz ⊢
  intro y hy
  induction hy using Algebra.adjoin_induction with
  | mem x hx => exact hz x hx
  | algebraMap r => exact commutes r z
  | add x y hx hy h₁ h₂ => simp [add_mul, mul_add, h₁, h₂]
  | mul x y hx hy h₁ h₂ => rw [← mul_assoc, ← h₁]; simp only [mul_assoc, h₂]

-- missing, and handy, we should have these for `adjoin/span/closure` and `ofClass` I think.
-- not marked `@[simp]` so that we don't introduce `ofClass` arbitrarily.
lemma Algebra.adjoin_subalgebra {R S A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
    [SetLike S A] [SubsemiringClass S A] [SMulMemClass S R A] (s : S) :
    adjoin R (s : Set A) = .ofClass s :=
  le_antisymm (adjoin_le <| by simp) subset_adjoin

-- missing, and handy, we should have these for the `ofClass` of the corresponding subobject.
@[simp]
lemma Subalgebra.ofClass_eq_self {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
    (s : Subalgebra R A) : Subalgebra.ofClass s = s := by
  simp [SetLike.ext'_iff]

lemma SubField.adjoin_centralizer_mul_comm (K D : Type*) [Field K] [DivisionRing D] [Algebra K D]
    (L : Subalgebra K D) (a : D) (ha : a ∈ Subalgebra.centralizer K L)
    (L_comm : ∀ x ∈ L, ∀ y ∈ L, x * y = y * x) :
    ∀ x ∈ Algebra.adjoin K (L ∪ {a}), ∀ y ∈ Algebra.adjoin K (L ∪ {a}), x * y = y * x := by
  simp_rw [← commute_iff_eq] at L_comm ⊢
  rw [forall₂_swap, ← le_centralizer_iff_commute] at L_comm ⊢
  simp only [adjoin_union, adjoin_subalgebra, ofClass_eq_self]
  refine sup_le_centralizer_self L_comm ?_ ?_
  · apply adjoin_le
    simp [- coe_centralizer, centralizer_adjoin, mem_centralizer_iff]
  · simpa [le_centralizer_iff, adjoin_le_iff]

-- note the first few lines of the previous proof are really just converting to the `centralizer` spelling
-- if you spell with centralizers, it's rather nice.
example (K D : Type*) [Field K] [DivisionRing D] [Algebra K D]
    (L : Subalgebra K D) (a : D) (ha : a ∈ Subalgebra.centralizer K L)
    (L_comm : L ≤ centralizer K L) :
    L ⊔ adjoin K {a} ≤ centralizer K ↑(L ⊔ adjoin K {a}):= by
  refine sup_le_centralizer_self L_comm ?_ ?_
  · apply adjoin_le
    simp [- coe_centralizer, centralizer_adjoin, mem_centralizer_iff]
  · simpa [le_centralizer_iff, adjoin_le_iff]

[Jireh Loreaux]

Note that, with the centralizer spelling, the iSup result becomes two lines, without a weird split into two hypotheses. And even jumping through the hoops to get the IsMulCommutative version you wrote is still less work with the centralizer approach.

lemma Subalgebra.iSup_le_centralizer_self {ι R A} [CommSemiring R] [Semiring A] [Algebra R A]
    {S : ι → Subalgebra R A} (h : ∀ i j, S i ≤ centralizer R (S j)) :
    (⨆ i, S i) ≤ centralizer R ↑(⨆ i, S i) := by
  rw [centralizer_coe_iSup]
  exact iSup_le fun i ↦ le_iInf fun j ↦ h i j

lemma Subalgebra.isComm_sup {ι R A} [CommSemiring R] [Semiring A] [Algebra R A]
    (S : ι → Subalgebra R A) (h₁ : ∀ i, IsMulCommutative (S i))
    (h₁₂ : Pairwise fun i j => ∀ x₁ ∈ S i, ∀ x₂ ∈ S j, Commute x₁ x₂) :
    IsMulCommutative ↥(⨆ i, S i) where
  is_comm := by
    refine ⟨?_⟩
    simp only [Subtype.forall, MulMemClass.mk_mul_mk, Subtype.mk.injEq]
    simp_rw [← commute_iff_eq]
    rw [forall₂_swap, ← Subalgebra.le_centralizer_iff_commute]
    apply Subalgebra.iSup_le_centralizer_self fun i j ↦ ?_
    obtain (rfl | h) := eq_or_ne j i
    · have := h₁ j |>.is_comm.comm
      simp at this
      rwa [Subalgebra.le_centralizer_iff_commute, forall₂_swap]
    · rw [Subalgebra.le_centralizer_iff_commute, forall₂_swap]
      exact h₁₂ h

[Kenny Lau]

@Jireh Loreaux I was thinking that maybe we were missing maybe Subalgebra.IsComm and SubAlgebra.IsDivisionRing; do you think these two yet-to-exist typeclasses might be in the wrong direction?

[Kenny Lau]

as in, I see that your plan to replace Subalgebra.IsComm is the idiom s <= centraliser s?

[Jireh Loreaux]

That's essentially what I'm arguing, yes.

[Eric Wieser]

One argument against that spelling is that s appears twice