English
There exists a unique SMulCandidate for any data α, φ, r, m at each object X, showing the scalar action is well defined.
Русский
Для каждой пары данных при каждом объекте X существует ровно один SMulCandidate, задающий скалярное действие корректно.
LaTeX
$$$ \forall X\; (r : (R.val.obj X).carrier)\; (m : (A.val.obj X).carrier), Unique (PresheafOfModules.Sheafify.SMulCandidate α φ r m) $$$
Lean4
theorem isCompatible_map_smul : ((r₀.smul m₀).map (whiskerRight φ (forget _))).Compatible :=
by
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ fac
let a₁ := r₀ f₁ h₁
let b₁ := m₀ f₁ h₁
let a₂ := r₀ f₂ h₂
let b₂ := m₀ f₂ h₂
let a₀ := R₀.map g₁.op a₁
let b₀ := M₀.map g₁.op b₁
have ha₁ : (α.app (Opposite.op Y₁)) a₁ = (R.map f₁.op) r := (hr₀ f₁ h₁).symm
have ha₂ : (α.app (Opposite.op Y₂)) a₂ = (R.map f₂.op) r := (hr₀ f₂ h₂).symm
have hb₁ : (φ.app (Opposite.op Y₁)) b₁ = (A.map f₁.op) m := (hm₀ f₁ h₁).symm
have hb₂ : (φ.app (Opposite.op Y₂)) b₂ = (A.map f₂.op) m := (hm₀ f₂ h₂).symm
have ha₀ : (α.app (Opposite.op Z)) a₀ = (R.map (f₁.op ≫ g₁.op)) r := by
rw [← RingCat.comp_apply, NatTrans.naturality, RingCat.comp_apply, ha₁, Functor.map_comp, RingCat.comp_apply]
have hb₀ : (φ.app (Opposite.op Z)) b₀ = (A.map (f₁.op ≫ g₁.op)) m :=
by
dsimp [b₀]
erw [NatTrans.naturality_apply φ, hb₁, Functor.map_comp, ConcreteCategory.comp_apply]
have ha₀' : (α.app (Opposite.op Z)) a₀ = (R.map (f₂.op ≫ g₂.op)) r := by rw [ha₀, ← op_comp, fac, op_comp]
have hb₀' : (φ.app (Opposite.op Z)) b₀ = (A.map (f₂.op ≫ g₂.op)) m := by rw [hb₀, ← op_comp, fac, op_comp]
dsimp
erw [← NatTrans.naturality_apply φ, ← NatTrans.naturality_apply φ]
exact
(isCompatible_map_smul_aux α φ hA r m f₁ g₁ a₁ a₀ b₁ b₀ ha₁ ha₀ hb₁ hb₀).trans
(isCompatible_map_smul_aux α φ hA r m f₂ g₂ a₂ a₀ b₂ b₀ ha₂ ha₀' hb₂ hb₀').symm
