Zulip Chat Archive

Stream: Is there code for X?

Topic: Induction over a generating set


Eric Wieser (Sep 30 2020 at 11:15):

If I have can show that sx is a generating set of a monoid X, is there an induction principle that can take something like ∀ x ∈ sx, p x, p 1, and ∀ x y, p x → p y → p (x * y) to produce ∀ x, p x? (and the same for algebras, rings, etc...)

Eric Wieser (Sep 30 2020 at 11:18):

I ended up building one myself for a special case in #4335, but the approach strikes me as obviously generalizable, and therefore likely to already exist.

Yury G. Kudryashov (Sep 30 2020 at 12:10):

See docs#submonoid.dense_induction

Patrick Massot (Sep 30 2020 at 13:39):

I don't think using "dense" is a good idea here. I think "generating" would be clearer.

Eric Wieser (Sep 30 2020 at 13:47):

Is there an equivalent for subrings and subalgebras?

Eric Wieser (Sep 30 2020 at 13:50):

docs#subring.closure_induction

Sebastien Gouezel (Sep 30 2020 at 13:51):

Also, the assumption is a little bit too strong, in ∀ (x y : M), p x → p y → p (x * y) one could also require that x belongs to s.

Eric Wieser (Sep 30 2020 at 13:55):

Should dense_induction be renamed to closure_induction to match?

Eric Wieser (Sep 30 2020 at 13:57):

Nevermind, I see that docs#submonoid.closure_induction already exists


Last updated: Dec 20 2023 at 11:08 UTC