comp_idx_apply

Mathlib.AlgebraicGeometry.Cover.MorphismProperty

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Cover.comp_idx_apply

Lean4

@[simp]
theorem comp_idx_apply {X : Scheme.{u}} {𝒰 𝒱 𝒲 : X.Cover (precoverage P)} (f : 𝒰 ⟶ 𝒱) (g : 𝒱 ⟶ 𝒲) (j : 𝒰.I₀) :
    (f ≫ g).idx j = g.idx (f.idx j) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru