From 3d05f49876adef4245c69b7f84df550e8b441cef Mon Sep 17 00:00:00 2001
From: Hu Yongle <2065545849@qq.com>
Date: Sat, 26 Oct 2024 09:38:58 +0800
Subject: [PATCH] init

---
 Others/Finite.lean             | 60 ++++++++++++++++++++++++++++++++++
 Others/FractionRing.lean       | 12 +++++++
 Others/Normal.lean             | 17 ++++++++++
 Others/restrictScalarsHom.lean | 29 ++++++++++++++++
 Others/separableClosure.lean   | 33 +++++++++++++++++++
 5 files changed, 151 insertions(+)
 create mode 100644 Others/Finite.lean
 create mode 100644 Others/FractionRing.lean
 create mode 100644 Others/Normal.lean
 create mode 100644 Others/restrictScalarsHom.lean
 create mode 100644 Others/separableClosure.lean

diff --git a/Others/Finite.lean b/Others/Finite.lean
new file mode 100644
index 0000000..618c4f8
--- /dev/null
+++ b/Others/Finite.lean
@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2024 Yongle Hu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yongle Hu
+-/
+import Mathlib.NumberTheory.NumberField.Basic
+
+section
+
+open Ideal
+
+attribute [local instance] Ideal.Quotient.field in
+/-- If `p` is a non-zero ideal of the `ℤ`, then `ℤ ⧸ p` is finite. -/
+theorem Int.Quotient.finite_of_ne_bot {I : Ideal ℤ} (h : I ≠ ⊥) : Finite (ℤ ⧸ I) := by
+  have equiv := Int.quotientSpanEquivZMod (Submodule.IsPrincipal.generator I)
+  rw [span_singleton_generator I] at equiv
+  haveI : NeZero (Submodule.IsPrincipal.generator I).natAbs := ⟨fun eq ↦
+    h ((Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero I).mpr (Int.natAbs_eq_zero.mp eq))⟩
+  exact Finite.of_equiv (ZMod (Submodule.IsPrincipal.generator I).natAbs) equiv.symm
+
+/-- In particular, if `p` is a maximal ideal of the `ℤ`, then `ℤ ⧸ p` is a finite field. -/
+instance Int.Quotient.finite_of_is_maxiaml (p : Ideal ℤ) [hpm : p.IsMaximal] :
+    Finite (ℤ ⧸ p) :=
+  finite_of_ne_bot (Ring.ne_bot_of_isMaximal_of_not_isField hpm Int.not_isField)
+
+/- #check Module.finite_of_finite
+#check FiniteDimensional.fintypeOfFintype
+def Module.Finite.finiteOfFinite {R M : Type*} [CommRing R] [Finite R] [AddCommMonoid M] [Module R M]
+    [Module.Finite R M] : Finite M := by
+  have := exists_fin' R M --exact .of_surjective f hf
+  sorry -/
+
+variable {R : Type*} [CommRing R] [h : Module.Finite ℤ R]
+
+theorem Ideal.Quotient.finite_of_module_finite_int {I : Ideal R} (hp : I ≠ ⊥) : Finite (R ⧸ I) := sorry
+
+-- `NoZeroSMulDivisors` can be removed
+instance Ideal.Quotient.finite_of_module_finite_int_of_isMaxiaml [NoZeroSMulDivisors ℤ R] [IsDomain R]
+    (p : Ideal R) [hpm : p.IsMaximal] : Finite (R ⧸ p) :=
+  Ideal.Quotient.finite_of_module_finite_int <| Ring.ne_bot_of_isMaximal_of_not_isField hpm <|
+    fun hf => Int.not_isField <|
+      (Algebra.IsIntegral.isField_iff_isField (NoZeroSMulDivisors.algebraMap_injective ℤ R)).mpr hf
+
+end
+
+namespace NumberField
+
+variable {K : Type*} [Field K] [NumberField K]
+
+/-- For any nonzero ideal `I` of `𝓞 K`, `(𝓞 K) ⧸ I` has only finite elements.
+  Note that if `I` is maximal, then `Finite ((𝓞 K) ⧸ I)` can be obtained by `inferInstance`. -/
+theorem quotientFiniteOfNeBot {I : Ideal (𝓞 K)} (h : I ≠ ⊥) : Finite ((𝓞 K) ⧸ I) :=
+  Ideal.Quotient.finite_of_module_finite_int h
+
+example (p : Ideal (𝓞 K)) [p.IsMaximal] : Finite ((𝓞 K) ⧸ p) := inferInstance
+
+/- instance quotientFiniteOfIsMaxiaml (p : Ideal (𝓞 K)) [hpm : p.IsMaximal] : Finite ((𝓞 K) ⧸ p) :=
+  quotientFiniteOfNeBot (Ring.ne_bot_of_isMaximal_of_not_isField hpm (RingOfIntegers.not_isField K)) -/
+
+end NumberField
diff --git a/Others/FractionRing.lean b/Others/FractionRing.lean
new file mode 100644
index 0000000..4d81864
--- /dev/null
+++ b/Others/FractionRing.lean
@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2024 Yongle Hu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yongle Hu
+-/
+import Mathlib.LinearAlgebra.FiniteDimensional.Defs
+
+attribute [local instance] FractionRing.liftAlgebra
+
+instance {A B : Type*} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B]
+    [Module.Finite A B] [NoZeroSMulDivisors A B] :
+    FiniteDimensional (FractionRing A) (FractionRing B) := sorry
diff --git a/Others/Normal.lean b/Others/Normal.lean
new file mode 100644
index 0000000..5f57b9a
--- /dev/null
+++ b/Others/Normal.lean
@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2024 Yongle Hu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yongle Hu
+-/
+import Mathlib.FieldTheory.PurelyInseparable
+import Mathlib.NumberTheory.NumberField.Basic
+import Mathlib.RingTheory.Valuation.ValuationRing
+
+attribute [local instance] Ideal.Quotient.field
+
+variable {A B : Type*} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B]
+  (p : Ideal A) (P : Ideal B) [p.IsMaximal] [P.IsMaximal] [P.LiesOver p]
+  (K L : Type*) [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] [Normal K L]
+
+example : Normal (A ⧸ p) (B ⧸ P) := sorry
diff --git a/Others/restrictScalarsHom.lean b/Others/restrictScalarsHom.lean
new file mode 100644
index 0000000..b94c9af
--- /dev/null
+++ b/Others/restrictScalarsHom.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2024 Yongle Hu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yongle Hu
+-/
+import Mathlib.Algebra.Algebra.Subalgebra.Tower
+import Mathlib.LinearAlgebra.Dimension.Finrank
+
+variable (R S A : Type*) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A]
+  [Algebra R A] [IsScalarTower R S A]
+
+def AlgEquiv.restrictScalarsHom : (A ≃ₐ[S] A) →* (A ≃ₐ[R] A) where
+  toFun f := AlgEquiv.restrictScalars R f
+  map_one' := rfl
+  map_mul' _ _ := rfl
+
+theorem AlgEquiv.restrictScalarsHom_injective : Function.Injective (AlgEquiv.restrictScalarsHom R S A) :=
+  AlgEquiv.restrictScalars_injective R
+
+theorem AlgEquiv.restrictScalarsHom_bot_surjective :
+    Function.Surjective (AlgEquiv.restrictScalarsHom R (⊥ : Subalgebra R S) S) := sorry
+
+noncomputable def subalgebra_bot_aut_equiv : (S ≃ₐ[(⊥ : Subalgebra R S)] S) ≃* (S ≃ₐ[R] S) :=
+  MulEquiv.ofBijective _
+    ⟨AlgEquiv.restrictScalarsHom_injective R _ S, AlgEquiv.restrictScalarsHom_bot_surjective R S⟩
+
+noncomputable def aut_equiv_of_finrank_eq_one {R S : Type*} (A : Type*) [CommSemiring R] [CommRing S]
+    [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A]
+    (h : Module.finrank R S = 1) : (A ≃ₐ[S] A) ≃* (A ≃ₐ[R] A) := sorry
diff --git a/Others/separableClosure.lean b/Others/separableClosure.lean
new file mode 100644
index 0000000..4645bb1
--- /dev/null
+++ b/Others/separableClosure.lean
@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2024 Yongle Hu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yongle Hu
+-/
+import Mathlib.FieldTheory.PurelyInseparable
+
+namespace separableClosure
+
+variable (K L : Type*) [Field K] [Field L] [Algebra K L] [Normal K L]
+
+#check IsPurelyInseparable.injective_comp_algebraMap
+
+#check instUniqueAlgHomOfIsPurelyInseparable
+
+#check separableClosure.isPurelyInseparable
+
+theorem restrictNormalHom_injective : Function.Injective
+    (AlgEquiv.restrictNormalHom (F := K) (K₁ := L) (separableClosure K L)) := by
+  sorry
+
+noncomputable def restrictNormalEquiv : (L ≃ₐ[K] L) ≃*
+    (separableClosure K L) ≃ₐ[K] (separableClosure K L) :=
+  MulEquiv.ofBijective _
+    ⟨restrictNormalHom_injective K L, AlgEquiv.restrictNormalHom_surjective L⟩
+
+example (e : PowerBasis K (separableClosure K L)) (σ τ : L ≃ₐ[K] L) (h : σ e.gen = τ e.gen) : σ = τ := by
+  sorry
+
+example [FiniteDimensional K L] : ∃ x : L, ∀ σ τ : L ≃ₐ[K] L, σ x = τ x → σ = τ := by
+  sorry
+
+end separableClosure