trans — Mathlib

English

If R ⊆ A ⊆ B is a tower and A → B is injective, then integrality descends from B to A.

Русский

Если R ⊆ A ⊆ B образуют башню и A→B инъективно, то интегральность спускается от B к A.

LaTeX

$$$\text{tower_bot}$$$

Lean4

protected theorem trans (hf : f.IsIntegral) (hg : g.IsIntegral) : (g.comp f).IsIntegral :=
  let _ := f.toAlgebra;
  let _ := g.toAlgebra;
  let _ := (g.comp f).toAlgebra
  have : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
  have : Algebra.IsIntegral R S := ⟨hf⟩
  have : Algebra.IsIntegral S T := ⟨hg⟩
  have : Algebra.IsIntegral R T := Algebra.IsIntegral.trans S
  Algebra.IsIntegral.isIntegral

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