forget_reflectsIsomorphisms — Mathlib

English

The forgetful functor forget LightProfinite reflects isomorphisms; i.e., if a morphism becomes an isomorphism after forgetting, it was already an isomorphism.

Русский

Функтор forget LightProfinite отражает изоморфизмы: если образ под забывающим функтором является изоморфизмом, то исходный морфизм тоже изоморфизм.

LaTeX

$$$\text{(forget LightProfinite).ReflectsIsomorphisms}$$$

Lean4

instance forget_reflectsIsomorphisms : (forget LightProfinite).ReflectsIsomorphisms :=
  by
  constructor
  intro A B f hf
  rw [isIso_iff_bijective] at hf
  exact LightProfinite.isIso_of_bijective _ hf

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