Submonoids

This file provides some results on multiplicative and additive submonoids in the finite context.

theorem Submonoid.pi_mem_of_mulSingle_mem_aux {η : Type u_1} {f : η → Type u_2} [(i : η) → MulOneClass (f i)] {S : Type u_3} [SetLike S ((i : η) → f i)] [SubmonoidClass S ((i : η) → f i)] [DecidableEq η] (I : Finset η) {H : S} (x : (i : η) → f i) (h1 : ∀ i ∉ I, x i = 1) (h2 : ∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) : x ∈ H

theorem AddSubmonoid.pi_mem_of_single_mem_aux {η : Type u_1} {f : η → Type u_2} [(i : η) → AddZeroClass (f i)] {S : Type u_3} [SetLike S ((i : η) → f i)] [AddSubmonoidClass S ((i : η) → f i)] [DecidableEq η] (I : Finset η) {H : S} (x : (i : η) → f i) (h1 : ∀ i ∉ I, x i = 0) (h2 : ∀ i ∈ I, Pi.single i (x i) ∈ H) : x ∈ H

theorem Submonoid.pi_mem_of_mulSingle_mem {η : Type u_1} {f : η → Type u_2} [(i : η) → MulOneClass (f i)] {S : Type u_3} [SetLike S ((i : η) → f i)] [SubmonoidClass S ((i : η) → f i)] [Finite η] [DecidableEq η] {H : S} (x : (i : η) → f i) (h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H) : x ∈ H

theorem AddSubmonoid.pi_mem_of_single_mem {η : Type u_1} {f : η → Type u_2} [(i : η) → AddZeroClass (f i)] {S : Type u_3} [SetLike S ((i : η) → f i)] [AddSubmonoidClass S ((i : η) → f i)] [Finite η] [DecidableEq η] {H : S} (x : (i : η) → f i) (h : ∀ (i : η), Pi.single i (x i) ∈ H) : x ∈ H

theorem Submonoid.pi_le_iff {η : Type u_1} {f : η → Type u_2} [(i : η) → MulOneClass (f i)] [Finite η] [DecidableEq η] {H : (i : η) → Submonoid (f i)} {J : Submonoid ((i : η) → f i)} : pi Set.univ H ≤ J ↔ ∀ (i : η), map (MonoidHom.mulSingle f i) (H i) ≤ J

For finite index types, the Submonoid.pi is generated by the embeddings of the monoids.

theorem AddSubmonoid.pi_le_iff {η : Type u_1} {f : η → Type u_2} [(i : η) → AddZeroClass (f i)] [Finite η] [DecidableEq η] {H : (i : η) → AddSubmonoid (f i)} {J : AddSubmonoid ((i : η) → f i)} : pi Set.univ H ≤ J ↔ ∀ (i : η), map (AddMonoidHom.single f i) (H i) ≤ J

For finite index types, the Submonoid.pi is generated by the embeddings of the additive monoids.

theorem Submonoid.closure_pi {η : Type u_1} {f : η → Type u_2} [(i : η) → MulOneClass (f i)] [Finite η] {s : (i : η) → Set (f i)} (hs : ∀ (i : η), 1 ∈ s i) : closure (Set.univ.pi fun (i : η) => s i) = pi Set.univ fun (i : η) => closure (s i)

theorem AddSubmonoid.closure_pi {η : Type u_1} {f : η → Type u_2} [(i : η) → AddZeroClass (f i)] [Finite η] {s : (i : η) → Set (f i)} (hs : ∀ (i : η), 0 ∈ s i) : closure (Set.univ.pi fun (i : η) => s i) = pi Set.univ fun (i : η) => closure (s i)