pairwiseDisjoint_leftCoset_cover_const_of_index_eq

English

If the index sum equals the size of the cover, then the finite-index cosets g_i H are pairwise disjoint.

Русский

Если сумма индексов равна размеру покрытия, то косеты с конечным индексом попарно неперекрывающие.

LaTeX

$$Set.PairwiseDisjoint (s.filter (fun i => (H i).FiniteIndex)) (fun i => g i • (H i))$$

Lean4

@[to_additive]
theorem pairwiseDisjoint_leftCoset_cover_const_of_index_eq (hind : H.index = s.card) :
    Set.PairwiseDisjoint s (g · • (H : Set G)) :=
  by
  have : Fintype (G ⧸ H) :=
    fintypeOfIndexNeZero fun h => by
      rw [hind, Finset.card_eq_zero] at h
      rw [h, ← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers
      exact Set.empty_ne_univ hcovers
  suffices Function.Bijective (g · : s → G ⧸ H)
    by
    intro i hi j hj h' c hi' hj' x hx
    specialize hi' hx
    specialize hj' hx
    rw [mem_leftCoset_iff, SetLike.mem_coe, ← QuotientGroup.eq] at hi' hj'
    rw [ne_eq, ← Subtype.mk.injEq (p := (· ∈ (s : Set ι))) i hi j hj] at h'
    exact h' <| this.injective <| by simp only [hi', hj']
  rw [Fintype.bijective_iff_surjective_and_card]
  constructor
  · rwa [leftCoset_cover_const_iff_surjOn, Set.surjOn_iff_surjective] at hcovers
  · simp only [Fintype.card_coe, ← hind, index_eq_card, Nat.card_eq_fintype_card]

Похожие утверждения