feat: Restriction of galois group onto integrally closed subrings. (#…

…9113)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Mathlib.lean

@@ -3070,6 +3070,7 @@ import Mathlib.RingTheory.Ideal.QuotientOperations
 import Mathlib.RingTheory.Int.Basic
 import Mathlib.RingTheory.IntegralClosure
 import Mathlib.RingTheory.IntegralDomain
+import Mathlib.RingTheory.IntegralRestrict
 import Mathlib.RingTheory.IntegrallyClosed
 import Mathlib.RingTheory.IsAdjoinRoot
 import Mathlib.RingTheory.IsTensorProduct

Mathlib/NumberTheory/NumberField/Basic.lean

@@ -146,7 +146,7 @@ instance : Free ℤ (𝓞 K) :=
   IsIntegralClosure.module_free ℤ ℚ K (𝓞 K)
 
 instance : IsLocalization (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) K :=
-  IsIntegralClosure.isLocalization ℤ ℚ K (𝓞 K)
+  IsIntegralClosure.isLocalization_of_isSeparable ℤ ℚ K (𝓞 K)
 
 /-- A ℤ-basis of the ring of integers of `K`. -/
 noncomputable def basis : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K) :=

Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

@@ -64,26 +64,31 @@ variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
 
 variable [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A C L]
 
-/- If `L` is a separable extension of `K = Frac(A)` and `L` has no zero smul divisors by `A`,
+/- If `L` is an algebraic extension of `K = Frac(A)` and `L` has no zero smul divisors by `A`,
 then `L` is the localization of the integral closure `C` of `A` in `L` at `A⁰`. -/
-theorem IsIntegralClosure.isLocalization [IsSeparable K L] [NoZeroSMulDivisors A L] :
+theorem IsIntegralClosure.isLocalization (hKL : Algebra.IsAlgebraic K L) :
     IsLocalization (Algebra.algebraMapSubmonoid C A⁰) L := by
   haveI : IsDomain C :=
     (IsIntegralClosure.equiv A C L (integralClosure A L)).toMulEquiv.isDomain (integralClosure A L)
+  haveI : NoZeroSMulDivisors A L := NoZeroSMulDivisors.trans A K L
   haveI : NoZeroSMulDivisors A C := IsIntegralClosure.noZeroSMulDivisors A L
   refine' ⟨_, fun z => _, fun {x y} h => ⟨1, _⟩⟩
   · rintro ⟨_, x, hx, rfl⟩
     rw [isUnit_iff_ne_zero, map_ne_zero_iff _ (IsIntegralClosure.algebraMap_injective C A L),
       Subtype.coe_mk, map_ne_zero_iff _ (NoZeroSMulDivisors.algebraMap_injective A C)]
     exact mem_nonZeroDivisors_iff_ne_zero.mp hx
   · obtain ⟨m, hm⟩ :=
-      IsIntegral.exists_multiple_integral_of_isLocalization A⁰ z (IsSeparable.isIntegral K z)
+      IsIntegral.exists_multiple_integral_of_isLocalization A⁰ z (hKL z).isIntegral
     obtain ⟨x, hx⟩ : ∃ x, algebraMap C L x = m • z := IsIntegralClosure.isIntegral_iff.mp hm
     refine' ⟨⟨x, algebraMap A C m, m, SetLike.coe_mem m, rfl⟩, _⟩
     rw [Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, hx, mul_comm, Submonoid.smul_def,
       smul_def]
   · simp only [IsIntegralClosure.algebraMap_injective C A L h]
-#align is_integral_closure.is_localization IsIntegralClosure.isLocalization
+
+theorem IsIntegralClosure.isLocalization_of_isSeparable [IsSeparable K L] :
+    IsLocalization (Algebra.algebraMapSubmonoid C A⁰) L :=
+  IsIntegralClosure.isLocalization A K L C (IsSeparable.isAlgebraic _ _)
+#align is_integral_closure.is_localization IsIntegralClosure.isLocalization_of_isSeparable
 
 variable [FiniteDimensional K L]
 
@@ -210,7 +215,7 @@ theorem IsIntegralClosure.rank [IsPrincipalIdealRing A] [NoZeroSMulDivisors A L]
   haveI : Module.Free A C := IsIntegralClosure.module_free A K L C
   haveI : IsNoetherian A C := IsIntegralClosure.isNoetherian A K L C
   haveI : IsLocalization (Algebra.algebraMapSubmonoid C A⁰) L :=
-    IsIntegralClosure.isLocalization A K L C
+    IsIntegralClosure.isLocalization A K L C (Algebra.IsIntegral.of_finite _ _).isAlgebraic
   let b := Basis.localizationLocalization K A⁰ L (Module.Free.chooseBasis A C)
   rw [FiniteDimensional.finrank_eq_card_chooseBasisIndex, FiniteDimensional.finrank_eq_card_basis b]
 #align is_integral_closure.rank IsIntegralClosure.rank

Mathlib/RingTheory/IntegralRestrict.lean

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2023 Andrew Yang, Patrick Lutz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.RingTheory.IntegrallyClosed
+import Mathlib.RingTheory.Norm
+import Mathlib.RingTheory.DedekindDomain.IntegralClosure
+/-!
+# Restriction of various maps between fields to integrally closed subrings.
+
+In this file, we assume `A` is an integrally closed domain; `K` is the fraction ring of `A`;
+`L` is a finite (separable) extension of `K`; `B` is the integral closure of `A` in `L`.
+We call this the AKLB setup.
+
+## Main definition
+- `galRestrict`: The restriction `Aut(L/K) → Aut(B/A)` as an `MulEquiv` in an AKLB setup.
+
+## TODO
+Define the restriction of norms and traces.
+
+-/
+open BigOperators nonZeroDivisors
+
+variable (A K L B : Type*) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
+    [Algebra A K] [IsFractionRing A K] [Algebra B L]
+    [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L]
+    [IsIntegralClosure B A L] [FiniteDimensional K L]
+
+/-- The lift `End(B/A) → End(L/K)` in an ALKB setup.
+This is inverse to the restriction. See `galRestrictHom`. -/
+noncomputable
+def galLift (σ : B →ₐ[A] B) : L →ₐ[K] L :=
+  haveI := (IsFractionRing.injective A K).isDomain
+  haveI := NoZeroSMulDivisors.trans A K L
+  haveI := IsIntegralClosure.isLocalization A K L B (Algebra.IsIntegral.of_finite _ _).isAlgebraic
+  haveI H : ∀ (y :  Algebra.algebraMapSubmonoid B A⁰),
+      IsUnit (((algebraMap B L).comp σ) (y : B)) := by
+    rintro ⟨_, x, hx, rfl⟩
+    simpa only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, AlgHom.commutes,
+      isUnit_iff_ne_zero, ne_eq, map_eq_zero_iff _ (NoZeroSMulDivisors.algebraMap_injective _ _),
+      ← IsScalarTower.algebraMap_apply] using nonZeroDivisors.ne_zero hx
+  haveI H_eq : (IsLocalization.lift (S := L) H).comp (algebraMap K L) = (algebraMap K L) := by
+    apply IsLocalization.ringHom_ext A⁰
+    ext
+    simp only [RingHom.coe_comp, Function.comp_apply, ← IsScalarTower.algebraMap_apply A K L,
+      IsScalarTower.algebraMap_apply A B L, IsLocalization.lift_eq,
+      RingHom.coe_coe, AlgHom.commutes]
+  { IsLocalization.lift (S := L) H with commutes' := FunLike.congr_fun H_eq }
+
+/-- The restriction `End(L/K) → End(B/A)` in an AKLB setup.
+Also see `galRestrict` for the `AlgEquiv` version. -/
+noncomputable
+def galRestrictHom : (L →ₐ[K] L) ≃* (B →ₐ[A] B) where
+  toFun := fun f ↦ (IsIntegralClosure.equiv A (integralClosure A L) L B).toAlgHom.comp
+      (((f.restrictScalars A).comp (IsScalarTower.toAlgHom A B L)).codRestrict
+        (integralClosure A L) (fun x ↦ IsIntegral.map _ (IsIntegralClosure.isIntegral A L x)))
+  map_mul' := by
+    intros σ₁ σ₂
+    ext x
+    apply (IsIntegralClosure.equiv A (integralClosure A L) L B).symm.injective
+    ext
+    dsimp
+    simp only [AlgEquiv.symm_apply_apply, AlgHom.coe_codRestrict, AlgHom.coe_comp,
+      AlgHom.coe_restrictScalars', IsScalarTower.coe_toAlgHom', Function.comp_apply,
+      AlgHom.mul_apply, IsIntegralClosure.algebraMap_equiv, Subalgebra.algebraMap_eq]
+    rfl
+  invFun := galLift A K L B
+  left_inv σ :=
+    have := (IsFractionRing.injective A K).isDomain
+    have := IsIntegralClosure.isLocalization A K L B (Algebra.IsIntegral.of_finite _ _).isAlgebraic
+    AlgHom.coe_ringHom_injective <| IsLocalization.ringHom_ext (Algebra.algebraMapSubmonoid B A⁰)
+      <| RingHom.ext fun x ↦ by simp [Subalgebra.algebraMap_eq, galLift]
+  right_inv σ :=
+    have := (IsFractionRing.injective A K).isDomain
+    have := IsIntegralClosure.isLocalization A K L B (Algebra.IsIntegral.of_finite _ _).isAlgebraic
+    AlgHom.ext fun x ↦
+      IsIntegralClosure.algebraMap_injective B A L (by simp [Subalgebra.algebraMap_eq, galLift])
+
+@[simp]
+lemma algebraMap_galRestrictHom_apply (σ : L →ₐ[K] L) (x : B) :
+    algebraMap B L (galRestrictHom A K L B σ x) = σ (algebraMap B L x) := by
+  simp [galRestrictHom, Subalgebra.algebraMap_eq]
+
+@[simp, nolint unusedHavesSuffices] -- false positive from unfolding galRestrictHom
+lemma galRestrictHom_symm_algebraMap_apply (σ : B →ₐ[A] B) (x : B) :
+    (galRestrictHom A K L B).symm σ (algebraMap B L x) = algebraMap B L (σ x) := by
+  have := (IsFractionRing.injective A K).isDomain
+  have := IsIntegralClosure.isLocalization A K L B (Algebra.IsIntegral.of_finite _ _).isAlgebraic
+  simp [galRestrictHom, galLift, Subalgebra.algebraMap_eq]
+
+/-- The restriction `Aut(L/K) → Aut(B/A)` in an AKLB setup. -/
+noncomputable
+def galRestrict : (L ≃ₐ[K] L) ≃* (B ≃ₐ[A] B) :=
+  (AlgEquiv.algHomUnitsEquiv K L).symm.trans
+    ((Units.mapEquiv <| galRestrictHom A K L B).trans (AlgEquiv.algHomUnitsEquiv A B))
+
+variable {K L}
+
+lemma coe_galRestrict_apply (σ : L ≃ₐ[K] L) :
+    (galRestrict A K L B σ : B →ₐ[A] B) = galRestrictHom A K L B σ := rfl
+
+variable {B}
+
+lemma galRestrict_apply (σ : L ≃ₐ[K] L) (x : B) :
+    galRestrict A K L B σ x = galRestrictHom A K L B σ x := rfl
+
+lemma algebraMap_galRestrict_apply (σ : L ≃ₐ[K] L) (x : B) :
+    algebraMap B L (galRestrict A K L B σ x) = σ (algebraMap B L x) :=
+  algebraMap_galRestrictHom_apply A K L B σ.toAlgHom x
+
+variable (K L B)
+
+lemma prod_galRestrict_eq_norm [IsGalois K L] [IsIntegrallyClosed A] (x : B) :
+    (∏ σ : L ≃ₐ[K] L, galRestrict A K L B σ x) =
+    algebraMap A B (IsIntegralClosure.mk' (R := A) A (Algebra.norm K <| algebraMap B L x)
+      (Algebra.isIntegral_norm K (IsIntegralClosure.isIntegral A L x).algebraMap)) := by
+  apply IsIntegralClosure.algebraMap_injective B A L
+  rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_eq A K L]
+  simp only [map_prod, algebraMap_galRestrict_apply, IsIntegralClosure.algebraMap_mk',
+    Algebra.norm_eq_prod_automorphisms, AlgHom.coe_coe, RingHom.coe_comp, Function.comp_apply]