adjoin_eq_Inf

Stream: Is there code for X?

[Andrew Yang]

Do we have this somewhere?

import ring_theory.adjoin.basic

lemma adjoin_eq_Inf {R S : Type*} [comm_semiring R] [semiring S] [algebra R S] (s : set S) :
  algebra.adjoin R s = Inf {p | s ⊆ p} :=
le_antisymm (le_Inf (λ _ h, algebra.adjoin_le h)) (Inf_le algebra.subset_adjoin)

[Adam Topaz]

Isn't this the definition of adjoin?

[Andrew Yang]

Its not. At least rfl does not work here. Its definition is

/-- The minimal subalgebra that includes `s`. -/
def adjoin (s : set A) : subalgebra R A :=
{ algebra_map_mem' := λ r, subsemiring.subset_closure $ or.inl ⟨r, rfl⟩,
  .. subsemiring.closure (set.range (algebra_map R A) ∪ s) }

[Adam Topaz]

I see... I guess we don't have that then.

I was under the impression that there should be an adjoin whenever there is a Galois insertion to set, and that it should always be defined as such an Inf, but in this case someone decided the definition should be in terms of subsemirings instead of subalgebras for some reason.

[Adam Topaz]

/-- The minimal subalgebra that includes s. -/ :expressionless:

[Eric Wieser]

We could use docs#subalgebra.copy in the implementation to make the lemma above rfl

[Eric Wieser]

Although I guess we could also just directly switch definition

[Anne Baanen]

I think docs#closure_operator or docs#lower_adjoint would help here.

[Anne Baanen]

That is, if we define adjoin to have type lower_adjoint (coe : subalgebra R A → set A), then we can derive this lemma from the Galois connection, right?

[Yaël Dillies]

Note that I'm not super happy with my current design of lower_adjoint, so feel free to suggest any change!

[Eric Wieser]

Do we have the associated galois_connection lemma already?

import ring_theory.adjoin.basic

-- do these exist somewhere with another name?
lemma is_least.Inf_eq {α : Type*} [complete_lattice α] {s : set α} {a : α} :
  is_least s a → Inf s = a
| ⟨ha, hal⟩ := le_antisymm (Inf_le ha) (le_Inf hal)

lemma is_greatest.Sup_eq {α : Type*} [complete_lattice α] {s : set α} {a : α} :
  is_greatest s a → Sup s = a :=
λ h, h.dual.Inf_eq

-- do we need these if the above exists?
lemma galois_connection.Inf_le_u_eq_l {α β : Type*} [preorder α] [complete_lattice β]
  {l : α → β} {u : β → α} (gc : galois_connection l u) (a : α) :
  Inf {b | a ≤ u b} = l a :=
gc.is_least_l.Inf_eq

lemma galois_connection.Sup_l_le_eq_u {α β : Type*} [complete_lattice α] [preorder β]
  {l : α → β} {u : β → α} (gc : galois_connection l u) (b : β) :
  Sup {a | l a ≤ b} = u b :=
gc.dual.Inf_le_u_eq_l _

-- the lemma in this thread
lemma adjoin_eq_Inf {R S : Type*} [comm_semiring R] [semiring S] [algebra R S] (s : set S) :
  algebra.adjoin R s = Inf {p | s ⊆ p} :=
((@algebra.gc R S _ _ _).Inf_le_u_eq_l s).symm

[Kevin Buzzard]

Oh nice!

[Eric Wieser]

Found a nicer proof using a missing is_least.Inf_eq

[Eric Wieser]

Ah, we have all the lemmas after all!

lemma adjoin_eq_Inf {R S : Type*} [comm_semiring R] [semiring S] [algebra R S] (s : set S) :
  algebra.adjoin R s = Inf {p | s ⊆ p} :=
(@algebra.gc R S _ _ _).is_glb_l.Inf_eq.symm