Show specific set forms a subspace iff some condition holds

Stream: new members

[Saif Ghobash]

I want to show that the set $\{(x_1,x_2,x_3,x_4) \in \mathbb{R}^4 : x_3 = 5x_4 + b\}$ forms a subspace iff $b=0$ (taken from Linear algebra done right). If I am not mistaken the syntax in lean for this set should be {x : fin 5 → ℝ | x 3 = 5*(x 4) + b}. I know that I cannot do something like this,

import algebra.module.basic
import algebra.module.submodule
import data.real.basic

example (b : ℝ) : b = 0 ↔ subspace {x : fin 5 → ℝ | x 3 = 5*(x 4) + b} :=
begin

end

Essentially I want to specify a specific carrier set and show that it forms a subspace iff some other condition holds. How would I write the statement of the question in LEAN?

[Alex J. Best]

fin 5 has five elements (0,1,2,3,4) so you probably want to use fin 4 instead and index from 0.

[Alex J. Best]

There isn't an is_subspace predicate in mathlib currently, possibly the easiest way to state this using the definitions in mathlib currently is to say that (submodule.span {x : fin 5 → ℝ | x 3 = 5*(x 4) + b} : set _) = {x : fin 5 → ℝ | x 3 = 5*(x 4) + b}. The span is the smallest subspace (module) containing the set so being equal to the span as a set is the same as being closed under the module operations

[Kyle Miller]

If you want to define a predicate, one possibility:

universes u v

/-- Does there exist an R-linear subspace with the given carrier set? -/
def is_subspace (R : Type u) {M : Type v} [field R] [add_comm_group M] [module R M]
  (s : set M) := ∃ (U : subspace R M), (U : set M) = s

example (b : ℝ) : b = 0 ↔ is_subspace ℝ {x : fin 3 → ℝ | x 3 = 5*(x 4) + b} :=
begin

end

[Alex J. Best]

You could alternatively phrase it as there exists a submodule that is equal as a set:

 ∃ s : submodule ℝ (fin 4 → ℝ), (s : set (fin 4 → ℝ)) = S

[Saif Ghobash]

@Alex J. Best @Kyle Miller Thank you for your help, both of these solutions should be enough for me :smile:

[Alex J. Best]

Oh nice I didn't know we had the abbreviation subspace for submodule, thats good

[Kyle Miller]

I haven't really done too much with algebra in Lean, so I had a go at the exercise.

I did it in a very hands-on way, but it would be conceptually nicer to use the fact that when b = 0 it's a subspace because it's the kernel of a linear map.

import algebra.module.basic
import algebra.module.submodule
import data.real.basic

universes u v

/-- Does there exist an R-linear subspace with the given carrier set? -/
def is_subspace (R : Type u) {M : Type v} [field R] [add_comm_group M] [module R M]
  (s : set M) := ∃ (U : subspace R M), (U : set M) = s

example (b : ℝ) : b = 0 ↔ is_subspace ℝ {x : fin 4 → ℝ | x 2 = 5*(x 3) + b} :=
begin
  by_cases hb : b = 0;
  simp only [hb, add_zero, true_iff, eq_self_iff_true, false_iff],
  { -- lean messes up the syntax if you don't give it the set explicitly
    refine ⟨⟨{x : fin 4 → ℝ | x 2 = 5*(x 3)},_,_,_⟩, rfl⟩,
    { simp, },
    { simp {contextual := tt},
      intros,
      ring, },
    { simp {contextual := tt},
      intros,
      ring, }, },
  { rintro ⟨⟨s, hzero, hadd, hbul⟩, hcarrier⟩,
    simp at hcarrier,
    subst s,
    simpa [ne.symm hb] using hzero, },
end

[Kyle Miller]

The proof is nicer if there's an is_subspace_iff lemma so you get easier access to the three axioms of a subspace.

lemma is_subspace_iff {R : Type u} {M : Type v} [field R] [add_comm_group M] [module R M]
  (s : set M) :
  is_subspace R s ↔
    (0 : M) ∈ s
    ∧ (∀ {a b}, a ∈ s → b ∈ s → a + b ∈ s)
    ∧ (∀ (c : R) {x}, x ∈ s → c • x ∈ s) :=
begin
  split,
  { rintro ⟨⟨carrier, hzero, hadd, hbul⟩, hcarrier⟩,
    simp only [submodule.coe_set_mk] at hcarrier,
    subst carrier,
    exact ⟨hzero, @hadd, hbul⟩, },
  { rintro ⟨hzero, hadd, hbul⟩,
    exact ⟨⟨s, hzero, @hadd, hbul⟩, rfl⟩, },
end

example (b : ℝ) : b = 0 ↔ is_subspace ℝ {x : fin 4 → ℝ | x 2 = 5*(x 3) + b} :=
begin
  rw is_subspace_iff,
  by_cases hb : b = 0,
  { simp [hb] {contextual := tt},
    refine ⟨_, _⟩; intros; ring, },
  { simp [hb, ne.symm hb] {contextual := tt}, },
end

[Kyle Miller]

It seems like predicates like is_subspace could be rather useful, since they expose carrier set for rewriting purposes. I know similar things are in the deprecated folder.

It's nice how you can easily turn an is_subspace R s into a subspace.

lemma is_subspace.to_subspace {R : Type u} {M : Type v} [field R] [add_comm_group M] [module R M]
  {s : set M} (h : is_subspace R s) : subspace R M :=
begin
  rw is_subspace_iff at h,
  exact ⟨s, h.1, h.2.1, h.2.2⟩,
end

[Kyle Miller]

I wonder what it would be like if mathlib's subobjects used a more unified interface, where there's an explicit predicate on carrier sets.

One possible design:

/-- it's `subtype` but with `carrier` rather than `val` -/
structure subobject {α : Type*} (p : set α → Prop) :=
(carrier : set α)
(property : p carrier)

/-- subobjects have a canonical set_like instance -/
instance subobject.set_like {α : Type*} (p : set α → Prop) : set_like (subobject p) α :=
⟨λ m, m.carrier, λ p q h, by cases p; cases q; congr'⟩

class foo (α : Type*) :=
(op : α → α)

structure is_subfoo (α : Type*) [foo α] (s : set α) : Prop :=
(op_mem : ∀ {x}, x ∈ s → foo.op x ∈ s)

def subfoo (α : Type*) [foo α] :=
subobject (is_subfoo α)

instance subfoo.set_like {α : Type*} [foo α] : set_like (subfoo α) α :=
subobject.set_like _

lemma subfoo.op_mem {α : Type*} [foo α] (m : subfoo α) {x} (h : x ∈ m) : foo.op x ∈ m :=
m.property.op_mem h

instance subfoo.foo {α} [foo α] (m : subfoo α) : foo m :=
⟨λ x, ⟨foo.op (x : α), m.op_mem x.property⟩⟩

[Kyle Miller]

(@Eric Wieser I guess this is another way set_like could work for subobjects)

[Anne Baanen]

I have also been thinking along these lines (also for morphisms). Some notes:

• it's not clear whether subfoo should be (semi)reducible:
• • if yes, then you'll create big unification problems easily (especially if it involves simp lemmas). I guess when using a structure type is_subfoo it's not too bad, but what about someone defining is_subring s := is_add_subgroup s ∧ is_submonoid s, is_add_subgroup s := is_add_monoid s ∧ ∀ x ∈ s, x⁻¹ ∈ s and is_add_monoid s := is_sub_additive s ∧ 0 ∈ s?
• • and if no, then you'll have to duplicate everything defined for subobject, resulting in more duplication
• there are relatively few things you have to duplicate per subobject that aren't handled through set_like: s.carrier = ↑s, the @[ext] lemma (could be solved with a smarter ext tactic, and the copy constructor.
• it doesn't really address the main source of duplication in my experience: for sub{semiring,ring,field} we (should) have finset_prod_mem, multiset_prod_mem, list_prod_mem, finset_sum_mem, multiset_sum_mem, list_sum_mem, polynomial_eval_mem, polynomial_eval₂_mem, polynomial_aeval_mem, finsupp_sum_mem, finsupp_total_mem, ...

[Anne Baanen]

So my conclusion is I'd be very happy to see someone else do this, but I'll first try out other ways to refactor subobjects, such as a per-subobject typeclass :)

[Eric Wieser]

I tried a refactor that included a closed_under (+) typeclass; the key thing we need the typeclass to state (or just provide) is that addition is the obvious addition induced by coercion. There's an open PR somewhere that doesn't build

[Anne Baanen]

Looks like #7834?

[Kyle Miller]

@Anne Baanen Do you think there's a missing feature in Lean that would help deal with all this duplication? I think there's no reason to believe that typeclasses are necessarily up to the task (as powerful as they may be). It might be like additive vs multiplicative structures, where we need generated lemmas to have the correct syntactic form -- one of the many issues with trying to use typeclasses for generic operations is that there's no head function for rw or simp.

One thing that's come to mind is having some way to write generalized theorems in some namespace, then having some metaprogramming command you can use to instantiate everything in that namespace with some substitutions that specialize the theorem statements, creating new theorems in the current namespace. It'd be like C++ templates (but the generic version is typechecked) or ML/OCaml functors (but implemented with metaprogramming).

One of the horrible things that the declare/def_declare thing supports with the simple way it's implemented is stringly typed (but easy) metaprogramming, like this example for set_like that I didn't share because I didn't want to give the wrong idea for what declare was supposed to be about:

def_declare subobject_set_like cls subcls :=
"
namespace %(subcls)
variables {X : Type*} [%(cls) X]

instance : set_like (%(subcls) X) X :=
⟨carrier, λ p q h, by cases p; cases q; congr'⟩

@[simp] lemma mem_carrier {p : %(subcls) X} {x : X} : x ∈ p.carrier ↔ x ∈ (p : set X) := iff.rfl

@[ext] theorem ext {p q : %(subcls) X} (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := set_like.ext h

/-- Copy of a `%(subcls)` with a new `carrier` equal to the old one. Useful to fix definitional
equalities. See Note [range copy pattern]. -/
protected def copy (p : %(subcls) X) (s : set X) (hs : s = ↑p) : %(subcls) X :=
{ carrier := s,
  op_mem' := hs.symm ▸ p.op_mem' }

@[simp] lemma coe_copy (p : %(subcls) X) (s : set X) (hs : s = ↑p) :
  (p.copy s hs : set X) = s := rfl

lemma copy_eq (p : %(subcls) X) (s : set X) (hs : s = ↑p) : p.copy s hs = p :=
set_like.coe_injective hs

end %(subcls)
"

class foo (α : Type*) :=
(op : α → α)

structure subfoo (α : Type*) [foo α] :=
(carrier : set α)
(op_mem' : ∀ {x}, x ∈ carrier → foo.op x ∈ carrier)

declare subobject_set_like foo subfoo

[Notification Bot]

This topic was moved by Anne Baanen to #general > Unified interface for subobjects