Does AlgEquiv has the IsInvariant instance?

Stream: Is there code for X?

[Junjie Bai]

Does this instance correct? If it is, how can I proof it?

import Mathlib

open Valued Valuation AlgEquiv WithZero

variable (K L : Type*) [Field K] [Field L]  [vK : Valued K ℤᵐ⁰] [vL : Valued L ℤᵐ⁰] [Algebra K L] [FiniteDimensional K L] [Normal K L] [Algebra.IsSeparable K L] [Valuation.HasExtension vK.v vL.v] [CompleteSpace K] [vK.v.IsNontrivial] [vL.v.IsNontrivial]
variable (σ : (L ≃ₐ[K] L)) {x : L} (hx : x ∈ vL.v.integer)

instance : Algebra.IsInvariant (↥𝒪[K]) (↥𝒪[L]) (↥𝒪[L] ≃ₐ[↥𝒪[K]] ↥𝒪[L]) := sorry

[Kevin Buzzard]

This doesn't compile for me on the web editor. I was a bit confused looking at the code because I saw both K and K', but I got errors on notation as well.

[Damiano Testa]

I think that there is a missing

open scoped WithZero

(found thanks to #find_syntax "ᵐ⁰") and possibly K' should be K?

[Junjie Bai]

Sorry for that. When I check it on web editor, I didn't notice that the editor is stopped so I ignore the errors. I have change my code.

[Thomas Browning]

You would just need to fill in this sorry:

import Mathlib

open Valued Valuation AlgEquiv WithZero

variable (K L : Type*) [Field K] [Field L]  [vK : Valued K ℤᵐ⁰] [vL : Valued L ℤᵐ⁰] [Algebra K L] [FiniteDimensional K L] [Normal K L] [Algebra.IsSeparable K L] [Valuation.HasExtension vK.v vL.v] [CompleteSpace K] [vK.v.IsNontrivial] [vL.v.IsNontrivial]
variable (σ : (L ≃ₐ[K] L)) {x : L} (hx : x ∈ vL.v.integer)

instance : Algebra.IsInvariant (↥𝒪[K]) (↥𝒪[L]) (↥𝒪[L] ≃ₐ[↥𝒪[K]] ↥𝒪[L]) := by
  have : IsGalois K L := by constructor
  have : IsIntegralClosure (↥𝒪[L]) (↥𝒪[K]) L :=
    sorry
  apply Algebra.isInvariant_of_isGalois' _ K L _

[Junjie Bai]

Thanks a lot!

[Yakov Pechersky]

We have docs#Valuation.isIntegrallyClosed_integers, the proof of which can help with the sorry here.

[Yakov Pechersky]

I realized we have some duplicate declarations, #29348 cleans that up

[Junjie Bai]

Thanks a lot!