map_ofFixingSubgroupUnion_bijective

English

For s,t with t ⊆ s there is an equivariant map from fixingSubgroup M s to fixingSubgroup M t induced by inclusion.

Русский

При t ⊆ s существует эквивариантное отображение из фиксационной подгруппы M s в фиксационную подгруппу M t, индуцированное включением.

LaTeX

$$$\\text{If } t \\subseteq s, \\text{ then there is an } \\mathrm{equivariant\_map} : ofFixingSubgroup(M,s) \\to_{\\text{inclusion}} ofFixingSubgroup(M,t).$$$

Lean4

@[to_additive]
theorem map_ofFixingSubgroupUnion_bijective : Bijective (map_ofFixingSubgroupUnion M s t) :=
  by
  constructor
  · intro a b h
    simpa only [← SetLike.coe_eq_coe] using h
  · rintro ⟨⟨a, ha⟩, ha'⟩
    suffices a ∈ ofFixingSubgroup M (s ∪ t) by exact ⟨⟨a, this⟩, rfl⟩
    intro hy
    rcases (Set.mem_union a s t).mp hy with h | h
    · exact ha h
    · apply ha'
      simpa only [Set.mem_preimage]

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