Theorems · Definition · number theory

WittVector.IsocrystalEquiv.mk.noConfusion

{p : ℕ} →
  {inst : Fact (Nat.Prime p)} →
    {k : Type u_1} →
      {inst_1 : CommRing k} →
        {inst_2 : CharP k p} →
          {inst_3 : PerfectRing k p} →
            {V : Type u_2} →
              {inst_4 : AddCommGroup V} →
                {inst_5 : WittVector.Isocrystal p k V} →
                  {V₂ : Type u_3} →
                    {inst_6 : AddCommGroup V₂} →
                      {inst_7 : WittVector.Isocrystal p k V₂} →
                        {P : Sort u} →
                          {toLinearEquiv : V ≃ₗ[FractionRing (WittVector p k)] V₂} →
                            {frob_equivariant :
                                ∀ (x : V),
                                  (WittVector.Isocrystal.frobenius p k) (toLinearEquiv x) =
                                    toLinearEquiv ((WittVector.Isocrystal.frobenius p k) x)} →
                              {toLinearEquiv' : V ≃ₗ[FractionRing (WittVector p k)] V₂} →
                                {frob_equivariant' :
                                    ∀ (x : V),
                                      (WittVector.Isocrystal.frobenius p k) (toLinearEquiv' x) =
                                        toLinearEquiv' ((WittVector.Isocrystal.frobenius p k) x)} →
                                  { toLinearEquiv := toLinearEquiv, frob_equivariant := frob_equivariant } =
                                      { toLinearEquiv := toLinearEquiv', frob_equivariant := frob_equivariant' } →
                                    (toLinearEquiv ≍ toLinearEquiv' → P) → P

Defined in

Mathlib.RingTheory.WittVector.Isocrystal

Cited by

1 results in Mathlib

Foundations

Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound