essFiniteType_iff_exists_subalgebra

English

EssFiniteType R S is equivalent to the existence of a finite subalgebra S0 and a localization M such that S is localized from S0 with FiniteType over R.

Русский

EssFiniteType R S эквивалентно существованию конечной подалгебры S0 и локализации M, так что S — локализация от S0 и FiniteType над R.

LaTeX

$$$EssFiniteType R S \iff \exists S_0:Subalgebra R S \;\exists M:Submonoid S_0,\; FiniteType R S_0 \land IsLocalization M S$$

Lean4

theorem essFiniteType_iff_exists_subalgebra :
    EssFiniteType R S ↔ ∃ (S₀ : Subalgebra R S) (M : Submonoid S₀), FiniteType R S₀ ∧ IsLocalization M S :=
  by
  refine ⟨fun h ↦ ⟨subalgebra R S, submonoid R S, inferInstance, inferInstance⟩, ?_⟩
  rintro ⟨S₀, M, _, _⟩
  letI := of_isLocalization S M
  exact comp R S₀ S

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