Intersection of subalgebras

Stream: new members

[Riccardo Brasca]

The following is true, right? I am a little bit lost since the lattice structure of subalgebra R A is done via Galois insertions, and I am not very familiar with them...

import algebra.algebra.subalgebra

variables {R : Type*} {A : Type*} [comm_semiring R] [semiring A] [algebra R A]
variables (S T : subalgebra R A)

lemma foo : (↑(S ⊓ T) : set A) = (S : set A) ∩ (T : set A) := sorry

[Kevin Buzzard]

Yes it's true :-)

[Riccardo Brasca]

I mean, for me ⊓ is the intersection (and for example for all other structures I checked it is defined this way). But for subalgebras everything is defined differently. For example we have explicitly docs#subring.has_Inf, but not for subalgebra (apply_instance find it, essentially going through docs#algebra.subalgebra.complete_lattice that uses docs#algebra.gi).

[Kevin Buzzard]

Yes, so the question becomes how galois_insertion.lift_complete_lattice makes the inf.

[Kevin Buzzard]

I think this is the definition being used:

def lift_semilattice_inf [semilattice_inf α] (gi : galois_insertion l u) : semilattice_inf β :=
{ inf := λ a b, gi.choice (u a ⊓ u b) $
    (le_inf (gi.gc.monotone_u $ gi.gc.l_le $ inf_le_left)
      (gi.gc.monotone_u $ gi.gc.l_le $ inf_le_right)),

[Kevin Buzzard]

I think it's easier just to redefine inf as the inter and use the axioms :-(

[Kevin Buzzard]

Unless you can figure out exactly what S ⊓ T : set A is

[Kevin Buzzard]

import algebra.algebra.subalgebra

variables {R : Type*} {A : Type*} [comm_semiring R] [semiring A] [algebra R A]
variables (S T : subalgebra R A)

lemma foo : (↑(S ⊓ T) : set A) = (S : set A) ∩ (T : set A) :=
begin
  let I : subalgebra R A :=
  { carrier := S ∩ T,
    add_mem' := λ _ _ ⟨hxS, hxT⟩ ⟨hyS, hyT⟩, ⟨S.add_mem' hxS hyS, T.add_mem' hxT hyT⟩,
    mul_mem' := λ _ _ ⟨hxS, hxT⟩ ⟨hyS, hyT⟩, ⟨S.mul_mem' hxS hyS, T.mul_mem' hxT hyT⟩,
    algebra_map_mem' := λ r, ⟨S.algebra_map_mem' r, T.algebra_map_mem' r⟩
  },
  suffices : S ⊓ T = I,
  { rw this, ext, refl },
  apply le_antisymm,
  { intros x hx, exact ⟨(inf_le_left : S ⊓ T ≤ S) hx, (inf_le_right : S ⊓ T ≤ T) hx⟩ },
  { exact le_inf (λ _ h, h.1) (λ _ h, h.2) }
end

bleurgh

[Yakov Pechersky]

import algebra.algebra.subalgebra

variables {R : Type*} {A : Type*} [comm_semiring R] [semiring A] [algebra R A]
variables (S T : subalgebra R A)

lemma foo : ((S ⊓ T) : set A) = (S : set A) ∩ (T : set A) :=
begin
  ext,
  simp
end

[Riccardo Brasca]

I am a little bit confused, but if you look at the infoview of your lemma, at the very beginning, it says ↑S ⊓ ↑T = ↑S ∩ ↑T. And indeed refl proves it.

[Riccardo Brasca]

In my lemma it says ↑(S ⊓ T) = ↑S ∩ ↑T

[Riccardo Brasca]

For some reasons when you say (S ⊓ T) : set A Lean understand ↑S ⊓ ↑T, so it is obvious.

[Ruben Van de Velde]

The issue is type ascription working outside-in; lean thinks you want the ⊓ that produces a set A, which is one that takes two set A's

[Yakov Pechersky]

You're right, apologies.

[Ruben Van de Velde]

Too bad :)

[Riccardo Brasca]

Don't worry, I quickly realized it because I did the same mistake :D

[Riccardo Brasca]

OK, this should work and it's less disgusting (the first two lemms should go there anyway).

import ring_theory.adjoin.basic

variables {R : Type*} {A : Type*} [comm_semiring R] [semiring A] [algebra R A]
variables (S T : subalgebra R A)

theorem adjoin_eq_of_le (S : subalgebra R A) (h₁ : s ⊆ S) (h₂ : S ≤ adjoin R s) : adjoin R s = S :=
le_antisymm (adjoin_le h₁) h₂

theorem adjoin_eq (S : subalgebra R A) : adjoin R ↑S = S :=
adjoin_eq_of_le _ (set.subset.refl _) subset_adjoin

lemma coe_inf (S T : subalgebra R A) : (↑(S ⊓ T) : set A) = (S : set A) ∩ (T : set A) :=
begin
  ext x,
  refine ⟨λ hx ,⟨_, _⟩, λ hx, _⟩,
  { have := @inf_le_left _ _ S T,
    exact this (set_like.mem_coe.1 hx) },
  { have := @inf_le_right _ _ S T,
    exact this (set_like.mem_coe.1 hx) },
  { have := @subset_adjoin R A _ _ _ ((S : set A) ∩ T),
    replace this := this hx,
    change x ∈ ↑(adjoin R (↑S ⊓ ↑T)) at this,
    rwa galois_insertion.l_inf_u (@algebra.gi R A _ _ _) at this }
end

[Yakov Pechersky]

import ring_theory.adjoin.basic

variables {R : Type*} {A : Type*} [comm_semiring R] [semiring A] [algebra R A]
variables (S T : subalgebra R A)

lemma coe_inf (S T : subalgebra R A) : (↑(S ⊓ T) : set A) = (S : set A) ∩ (T : set A) :=
begin
  apply le_antisymm,
  { simp },
  { rw ←galois_insertion.l_inf_u (@algebra.gi R A _ _ _),
    exact algebra.subset_adjoin }
end

[Riccardo Brasca]

Nice!!

[Yakov Pechersky]

I try to avoid change, because it can hide expensive refls. If the underlying definitions change, then change can easily break or become much slower.

[Yakov Pechersky]

Instead, doing the appropriate rw will always work

[Eric Wieser]

It seems to me that it might still be worth redefining inf as the version defeq to set intersection

[Eric Wieser]

Especially since we do it everwhere else

[Kevin Buzzard]

I think this is the canonical problem with this clever "make subwidgets into a complete lattice by using the Galois insertion into set" approach -- Sup is defined to be "intersection of subwidgets containing your given subwidget" but somehow everything else ends up out of control.

[Riccardo Brasca]

I will try to do this. I agree that it's not clear which one is the better approach... in any case not everything is the same for (say) submodules and subalgebras: for example ⊥.prod ⊥ = ⊥ is trivially true for submodules but false for subalgebras.

[Eric Wieser]

#7812 makes foo (aka coe_inf) true by rfl