liftCLM — Mathlib

English

Given a map f : M →SL[σ] N which is compatible with inseparable pairs, there is a lift CLM: SeparationQuotient M →SL[σ] N extending f.

Русский

Для отображения f : M →SL[σ] N существовaет подъем CLM: SeparationQuotient M →SL[σ] N, который продолжает f.

LaTeX

$$$\mathrm{liftCLM}:\, M \toSL[\sigma] N \Rightarrow \mathrm{SeparationQuotient}M \toSL[\sigma] N$$$

Lean4

/-- The lift (as a continuous linear map) of `f` with `f x = f y` for `Inseparable x y`. -/
@[simps]
noncomputable def liftCLM {σ : R →+* S} (f : M →SL[σ] N) (hf : ∀ x y, Inseparable x y → f x = f y) :
    SeparationQuotient M →SL[σ] N where
  toFun := SeparationQuotient.lift f hf
  map_add' := Quotient.ind₂ <| map_add f
  map_smul' {r} := Quotient.ind <| map_smulₛₗ f r

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