## Stream: new members

### Topic: Show specific set forms a subspace iff some condition holds

#### Saif Ghobash (Nov 28 2021 at 17:11):

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 (Nov 28 2021 at 17:17):

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 (Nov 28 2021 at 17:19):

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 (Nov 28 2021 at 17:22):

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 (Nov 28 2021 at 17:22):

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 (Nov 28 2021 at 17:24):

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

#### Alex J. Best (Nov 28 2021 at 17:24):

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

#### Kyle Miller (Nov 28 2021 at 17:36):

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.

#### Kyle Miller (Nov 28 2021 at 17:50):

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 ⟨⟨s, hzero, @hadd, hbul⟩, rfl⟩, },
end


#### Kyle Miller (Nov 28 2021 at 18:00):

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 (Nov 28 2021 at 18:30):

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 (Nov 28 2021 at 18:39):

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

#### Anne Baanen (Nov 29 2021 at 11:45):

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 (Nov 29 2021 at 11:46):

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 (Nov 29 2021 at 13:40):

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 (Nov 29 2021 at 13:56):

Looks like #7834?

#### Kyle Miller (Nov 29 2021 at 18:18):

@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 (Nov 30 2021 at 11:01):

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

Last updated: Dec 20 2023 at 11:08 UTC