theorem
L35 ↗appLE_of_comp_eq
AlgebraicGeometry.SmallExtension.IsFibreReading.appLE_of_comp_eq
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs.SmallExtension_IsFibreReading_appLE_of_comp_eq
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe uLean source · statement
theorem _root_.AlgebraicGeometry.SmallExtension.IsFibreReading.appLE_of_comp_eq
{B₁ : Type u} [CommRing B₁] {k : Type u} [Field k]
(V : Type u) [AddCommGroup V] [Module k V] [Module B₁ V] (ι : V →ₗ[B₁] B₁)
{X X' Xk Xk' : Scheme.{u}}
(f : X ⟶ Spec (CommRingCat.of B₁)) (f' : X' ⟶ Spec (CommRingCat.of B₁))
(fk : Xk ⟶ Spec (CommRingCat.of k)) (fk' : Xk' ⟶ Spec (CommRingCat.of k))
(i : Xk ⟶ X) (i' : Xk' ⟶ X')
(h : X' ⟶ X) (hh : h ≫ f = f')
(hk : Xk' ⟶ Xk) (hhk : hk ≫ i = i' ≫ h) (hfk : hk ≫ fk = fk')
(U : X.Opens) (W : Xk.Opens) (hW : W ≤ i ⁻¹ᵁ U)
(U' : X'.Opens) (hU' : U' ≤ h ⁻¹ᵁ U) (W' : Xk'.Opens) (hW' : W' ≤ i' ⁻¹ᵁ U') (hWk : W' ≤ hk ⁻¹ᵁ
W)
(δ : Γ(X, U)) (w : Module.Dual k V →ₗ[k] (OModulePresheaf.unit fk).obj W)
(w' : Module.Dual k V →ₗ[k] (OModulePresheaf.unit fk').obj W')
(hw' : ∀ ξ : Module.Dual k V, w' ξ = (hk.appLE W W' hWk).hom (w ξ))
(hw : IsFibreReading V ι f fk i U W hW δ w) :
IsFibreReading V ι f' fk' i' U' W' hW' ((h.appLE U U' hU').hom δ) w'