English
A generalisation of the identity map that constructs the identity as a σ-semilinear map when σ is the identity ring homomorphism.
Русский
Обобщение идентичного отображения, строящего идентичность как σ-симилинейное отображение, когда σ — тождественное гомоморфизм кольца.
LaTeX
$$$\mathrm{id'}\!_{\sigma}: M \to_\sigma M$ is the identity semilinear map when σ = id$$$
Lean4
/-- A generalisation of `LinearMap.id` that constructs the identity function
as a `σ`-semilinear map for any ring homomorphism `σ` which we know is the identity. -/
@[simps]
def id' {σ : R →+* R} [RingHomId σ] : M →ₛₗ[σ] M where
toFun x := x
map_add' _ _ := rfl
map_smul' r
x := by
have := (RingHomId.eq_id : σ = _)
subst this
rfl
