Standard usage of induction for quotient algebraic structure

Stream: new members

[Xingyu Zhong]

In the middle of a proof, to treat some element of a quotient type as an application of the canonical quotient map, Quotient.inductionOn is used. For example, in the tactic mode,

induction' y using Quotient.inductionOn with x

where y is an element in a quotient type.

I'm wondering if there is a standard way to lift elements of a quotient algebraic structure such as quotient groups and quotient modules. I notice that there are corresponding induction_on-like theorems in Mathlib, e.g.

#check QuotientGroup.induction_on
#check Submodule.Quotient.induction_on

Are they supposed to be used for induction purpose? In practice I see lots of people still use Quotient.inductionOn directly when working with quotient algebraic structures. Up to definitional equality this won't make a difference, But I'm still interested in a textbook approach.

Another question is that, since we have upgraded versions of Quotient.lift in Mathlib that lift the bundled homomorphisms

#check QuotientGroup.lift
#check Submodule.liftQ

why there aren't any upgraded version of Quotient.inductionOn that, for example, allow us to treat any element in a quotient module M ⧸ p as some application of p.mkQ?

variable {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M)
theorem Submodule.Quotient.my_induction_on {C : M ⧸ p → Prop} (x : M ⧸ p) (H : ∀ z, C (p.mkQ z)) : C x := Quotient.inductionOn' x H

After all, it respects scalar multiplication and addition. Wouldn't this be a better induction rule to live in Mathlib?

Appreciate your help!

[Aaron Liu]

Xingyu Zhong said:

why there aren't any upgraded version of Quotient.inductionOn that, for example, allow us to treat any element in a quotient module M ⧸ p as some application of p.mkQ?

You can use docs#Submodule.mkQ_surjective

[Yuyang Zhao]

We will have general quotient lemmas if we can merge #30668. :innocent:

[Yuyang Zhao]

Ah, bundled homomorphisms still need to be defined separately. But bundled mkQ is usually simp to a non-bundled function. Currently docs#QuotientGroup.coe_mk' docs#Submodule.mkQ_apply are simp lemmas.