inhabited — Mathlib

English

There is an instance giving the minimal extension construction on the Baer extensions lattice, via infimum of linear partial maps.

Русский

Существует инстанс минимального расширения в решётке расширений Баера, через инфимум линейных частичных отображений.

LaTeX

$$$ \text{Min ExtensionOf } i f$$$

Lean4

instance inhabited : Inhabited (ExtensionOf i f) where
  default :=
    { domain := LinearMap.range i
      toFun :=
        { toFun := fun x => f x.2.choose
          map_add' := fun x y =>
            by
            have eq1 : _ + _ = (x + y).1 := congr_arg₂ (· + ·) x.2.choose_spec y.2.choose_spec
            rw [← map_add, ← (x + y).2.choose_spec] at eq1
            dsimp
            rw [← Fact.out (p := Function.Injective i) eq1, map_add]
          map_smul' := fun r x =>
            by
            have eq1 : r • _ = (r • x).1 := congr_arg (r • ·) x.2.choose_spec
            rw [← LinearMap.map_smul, ← (r • x).2.choose_spec] at eq1
            dsimp
            rw [← Fact.out (p := Function.Injective i) eq1, LinearMap.map_smul] }
      le := le_refl _
      is_extension := fun m => by
        simp only [LinearPMap.mk_apply, LinearMap.coe_mk]
        dsimp
        apply congrArg
        exact Fact.out (p := Function.Injective i) (⟨i m, ⟨_, rfl⟩⟩ : LinearMap.range i).2.choose_spec.symm }

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