import Definitions.Def_CuspForm_AuxLevelHeckeModule set_option autoImplicit false noncomputable section namespace CuspForm.AuxLevel def midOp (N r : β„•) (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] (g : Gen N r S) : Module.End π’ͺ (CohCarrier.H1 (N * r) ⊀ π’ͺ) := haveI : NeZero g.β„“ := ⟨g.prime.ne_zero⟩ CohCarrier.heckeTL (N * r) ⊀ π’ͺ g.β„“ def MidOpComm (N r : β„•) (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] : Prop := βˆ€ g h : Gen N r S, midOp N r S π’ͺ g * midOp N r S π’ͺ h = midOp N r S π’ͺ h * midOp N r S π’ͺ g def midHeckeData (N r : β„•) [NeZero N] (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ] (ΞΈ : β†₯(CuspForm.heckeAlgebra N 2 S) β†’+* IsLocalRing.ResidueField π’ͺ) (hc₁ : MidOpComm N r S π’ͺ) : CohCarrier.HeckeData π’ͺ (CohCarrier.H1 (N * r) ⊀ π’ͺ) (IsLocalRing.ResidueField π’ͺ) where Gen := Gen N r S op := midOp N r S π’ͺ comm := hc₁ ΞΈbar g := ΞΈ (CuspForm.heckeAlgebra.T g.prime g.not_dvd g.notMem) instance instModuleFreeAlgMidCarrier (N r : β„•) [NeZero N] (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ] (ΞΈ : β†₯(CuspForm.heckeAlgebra N 2 S) β†’+* IsLocalRing.ResidueField π’ͺ) (hc₁ : MidOpComm N r S π’ͺ) : Module (midHeckeData N r S π’ͺ ΞΈ hc₁).FreeAlg (CohCarrier.H1 (N * r) ⊀ π’ͺ) := (midHeckeData N r S π’ͺ ΞΈ hc₁).moduleFreeAlg abbrev midML (N r : β„•) [NeZero N] (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ] (ΞΈ : β†₯(CuspForm.heckeAlgebra N 2 S) β†’+* IsLocalRing.ResidueField π’ͺ) (hc₁ : MidOpComm N r S π’ͺ) : Type := (midHeckeData N r S π’ͺ ΞΈ hc₁).ML example (N r : β„•) [NeZero N] (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ] (ΞΈ : β†₯(CuspForm.heckeAlgebra N 2 S) β†’+* IsLocalRing.ResidueField π’ͺ) (hc₁ : MidOpComm N r S π’ͺ) (hc : OpComm N r S π’ͺ) : (midHeckeData N r S π’ͺ ΞΈ hc₁).FreeAlg = (heckeData N r S π’ͺ ΞΈ hc).FreeAlg := rfl example (N r : β„•) [NeZero N] (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ] (ΞΈ : β†₯(CuspForm.heckeAlgebra N 2 S) β†’+* IsLocalRing.ResidueField π’ͺ) (hc₁ : MidOpComm N r S π’ͺ) (hc : OpComm N r S π’ͺ) : (midHeckeData N r S π’ͺ ΞΈ hc₁).mTheta = (heckeData N r S π’ͺ ΞΈ hc).mTheta := rfl example (N r : β„•) [NeZero N] (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ] (ΞΈ : β†₯(CuspForm.heckeAlgebra N 2 S) β†’+* IsLocalRing.ResidueField π’ͺ) (hc₁ : MidOpComm N r S π’ͺ) : Module π’ͺ (midML N r S π’ͺ ΞΈ hc₁) := by infer_instance example (N r : β„•) [NeZero N] (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ] (ΞΈ : β†₯(CuspForm.heckeAlgebra N 2 S) β†’+* IsLocalRing.ResidueField π’ͺ) (hc₁ : MidOpComm N r S π’ͺ) : Module (midHeckeData N r S π’ͺ ΞΈ hc₁).FreeAlg (midML N r S π’ͺ ΞΈ hc₁) := by infer_instance example (N r : β„•) [NeZero N] (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ] (ΞΈ : β†₯(CuspForm.heckeAlgebra N 2 S) β†’+* IsLocalRing.ResidueField π’ͺ) (hc₁ : MidOpComm N r S π’ͺ) : IsScalarTower π’ͺ (midHeckeData N r S π’ͺ ΞΈ hc₁).FreeAlg (midML N r S π’ͺ ΞΈ hc₁) := by infer_instance end CuspForm.AuxLevel end