ofFixingSubgroup_of_eq — Mathlib

English

There is an equality correspondence between fixing subgroups under equal sets, realized as an equivariant map.

Русский

Существует равенство фиксационных подгрупп при равных множествах, реализуемое как эквивариантное отображение.

LaTeX

$$$\text{Eq fixingSubgroup map}$$$

Lean4

/-- The identity between the `SubMulAction`s of `fixingSubgroup`s
of equal sets, as an equivariant map. -/
@[to_additive /-- The identity between the `SubAddAction`s of `fixingAddSubgroup`s
    of equal sets, as an equivariant map. -/
    ]
def ofFixingSubgroup_of_eq (hst : s = t) :
    let φ : fixingSubgroup M s ≃* fixingSubgroup M t := MulEquiv.subgroupCongr (congrArg₂ _ rfl hst)
    ofFixingSubgroup M s →ₑ[φ] ofFixingSubgroup M t
    where
  toFun := fun ⟨x, hx⟩ => ⟨x, by rw [← hst]; exact hx⟩
  map_smul' := fun ⟨m, hm⟩ ⟨x, hx⟩ => rfl

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