CompletedFrobeniusLift.lean

def padicCompletedLevelOriginalAlgebra
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Algebra (padicCompletedUnramifiedField p)
      (padicCompletedLevelField p n)

def padicCompletedLevelFrobeniusAlgebra
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Algebra (padicCompletedUnramifiedField p)
      (padicCompletedLevelField p n)

theorem padicCompletedLevelFrobeniusAlgebra_algebraMap
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : padicCompletedUnramifiedField p) :
    @algebraMap
        (padicCompletedUnramifiedField p)
        (padicCompletedLevelField p n)
        _ _ (padicCompletedLevelFrobeniusAlgebra p n) a =
      algebraMap (padicCompletedUnramifiedField p)
        (padicCompletedLevelField p n)
        (padicCompletedUnramifiedFrobenius p a)

theorem padicCompletedPrimitivePolynomial_frobenius
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicCompletedPrimitivePolynomial p n).map
        (padicCompletedUnramifiedFrobenius p).toAlgHom.toRingHom =
      padicCompletedPrimitivePolynomial p n

theorem padicCompletedUnitParameterRoot_aeval_minpoly_frobenius
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    @Polynomial.aeval
        (padicCompletedUnramifiedField p)
        (padicCompletedLevelField p n)
        _ _ (padicCompletedLevelFrobeniusAlgebra p n)
        (padicCompletedUnitParameterRoot p n a)
        (minpoly (padicCompletedUnramifiedField p)
          (padicCompletedPrimitiveRoot p n)) =
      0

def padicCompletedFrobeniusLiftAlgHom
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    @AlgHom
      (padicCompletedUnramifiedField p)
      (padicCompletedLevelField p n)
      (padicCompletedLevelField p n)
      _ _ _
      (padicCompletedLevelOriginalAlgebra p n)
      (padicCompletedLevelFrobeniusAlgebra p n)

theorem padicCompletedFrobeniusLiftAlgHom_primitiveRoot
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    padicCompletedFrobeniusLiftAlgHom p n a
        (padicCompletedPrimitiveRoot p n) =
      padicCompletedUnitParameterRoot p n a

def padicCompletedFrobeniusLift
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    padicCompletedLevelField p n →+*
      padicCompletedLevelField p n

theorem padicCompletedFrobeniusLift_algebraMap
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n)
    (b : padicCompletedUnramifiedField p) :
    padicCompletedFrobeniusLift p n a
        (algebraMap (padicCompletedUnramifiedField p)
          (padicCompletedLevelField p n) b) =
      algebraMap (padicCompletedUnramifiedField p)
        (padicCompletedLevelField p n)
        (padicCompletedUnramifiedFrobenius p b)

theorem padicCompletedFrobeniusLift_primitiveRoot
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    padicCompletedFrobeniusLift p n a
        (padicCompletedPrimitiveRoot p n) =
      padicCompletedUnitParameterRoot p n a

theorem padicCompletedFrobeniusLift_surjective
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    Function.Surjective (padicCompletedFrobeniusLift p n a)

def padicCompletedFrobeniusLiftEquiv
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    padicCompletedLevelField p n ≃+*
      padicCompletedLevelField p n

theorem padicCompletedFrobeniusLiftEquiv_algebraMap
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n)
    (b : padicCompletedUnramifiedField p) :
    padicCompletedFrobeniusLiftEquiv p n a
        (algebraMap (padicCompletedUnramifiedField p)
          (padicCompletedLevelField p n) b) =
      algebraMap (padicCompletedUnramifiedField p)
        (padicCompletedLevelField p n)
        (padicCompletedUnramifiedFrobenius p b)

theorem padicCompletedFrobeniusLiftEquiv_primitiveRoot
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    padicCompletedFrobeniusLiftEquiv p n a
        (padicCompletedPrimitiveRoot p n) =
      padicCompletedUnitParameterRoot p n a

theorem
    padicCompletedStandardPrimitivePointUnitAction_aeval_minpoly_frobenius
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    @Polynomial.aeval
        (padicCompletedUnramifiedField p)
        (padicCompletedLevelField p n)
        _ _ (padicCompletedLevelFrobeniusAlgebra p n)
        (((padicCompletedStandardPrimitivePointUnitAction p n u :
            (padicCompletedLevelCompleteDVF p n).valuationSubring) :
          padicCompletedLevelField p n))
        (minpoly (padicCompletedUnramifiedField p)
          (padicCompletedPrimitiveRoot p n)) =
      0

def padicCompletedUnitFrobeniusLiftAlgHom
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    @AlgHom
      (padicCompletedUnramifiedField p)
      (padicCompletedLevelField p n)
      (padicCompletedLevelField p n)
      _ _ _
      (padicCompletedLevelOriginalAlgebra p n)
      (padicCompletedLevelFrobeniusAlgebra p n)

theorem padicCompletedUnitFrobeniusLiftAlgHom_primitiveRoot
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    padicCompletedUnitFrobeniusLiftAlgHom p n u
        (padicCompletedPrimitiveRoot p n) =
      (((padicCompletedStandardPrimitivePointUnitAction p n u :
          (padicCompletedLevelCompleteDVF p n).valuationSubring) :
        padicCompletedLevelField p n))

def padicCompletedUnitFrobeniusLift
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    padicCompletedLevelField p n →+*
      padicCompletedLevelField p n

theorem padicCompletedUnitFrobeniusLift_algebraMap
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (b : padicCompletedUnramifiedField p) :
    padicCompletedUnitFrobeniusLift p n u
        (algebraMap (padicCompletedUnramifiedField p)
          (padicCompletedLevelField p n) b) =
      algebraMap (padicCompletedUnramifiedField p)
        (padicCompletedLevelField p n)
        (padicCompletedUnramifiedFrobenius p b)

theorem padicCompletedUnitFrobeniusLift_primitiveRoot
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    padicCompletedUnitFrobeniusLift p n u
        (padicCompletedPrimitiveRoot p n) =
      (((padicCompletedStandardPrimitivePointUnitAction p n u :
          (padicCompletedLevelCompleteDVF p n).valuationSubring) :
        padicCompletedLevelField p n))

theorem padicCompletedUnitFrobeniusLift_surjective
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    Function.Surjective (padicCompletedUnitFrobeniusLift p n u)

def padicCompletedUnitFrobeniusLiftEquiv
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    padicCompletedLevelField p n ≃+*
      padicCompletedLevelField p n

theorem padicCompletedUnitFrobeniusLiftEquiv_algebraMap
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (b : padicCompletedUnramifiedField p) :
    padicCompletedUnitFrobeniusLiftEquiv p n u
        (algebraMap (padicCompletedUnramifiedField p)
          (padicCompletedLevelField p n) b) =
      algebraMap (padicCompletedUnramifiedField p)
        (padicCompletedLevelField p n)
        (padicCompletedUnramifiedFrobenius p b)

theorem padicCompletedUnitFrobeniusLiftEquiv_primitiveRoot
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    padicCompletedUnitFrobeniusLiftEquiv p n u
        (padicCompletedPrimitiveRoot p n) =
      (((padicCompletedStandardPrimitivePointUnitAction p n u :
          (padicCompletedLevelCompleteDVF p n).valuationSubring) :
        padicCompletedLevelField p n))