import Mathlib import Definitions.Def_GaloisRep_Adic set_option autoImplicit false noncomputable section namespace GaloisRep open IsLocalRing variable (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ] structure IsArtinianTestAlgebra (A : Type) [CommRing A] [IsLocalRing A] [Algebra π’ͺ A] : Prop where isLocalHom : IsLocalHom (algebraMap π’ͺ A) residue_surjective : Function.Surjective (IsLocalRing.residue A ∘ algebraMap π’ͺ A) isArtinian : IsArtinianRing A structure IsDeformationCondition (π’Ÿ : βˆ€ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [Algebra π’ͺ A], GaloisRepAdic A β†’ Prop) : Prop where of_isEquiv : βˆ€ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [Algebra π’ͺ A], IsArtinianTestAlgebra π’ͺ A β†’ βˆ€ ⦃ρ ρ' : GaloisRepAdic A⦄, ρ.IsEquiv ρ' β†’ π’Ÿ ρ β†’ π’Ÿ ρ' baseChangeAlong : βˆ€ ⦃A B : Type⦄ [CommRing A] [IsLocalRing A] [Algebra π’ͺ A] [CommRing B] [IsLocalRing B] [Algebra π’ͺ B], IsArtinianTestAlgebra π’ͺ A β†’ IsArtinianTestAlgebra π’ͺ B β†’ βˆ€ (Ο† : A →ₐ[π’ͺ] B) (hΟ† : IsLocalHom (Ο† : A β†’+* B)) ⦃ρ : GaloisRepAdic A⦄, π’Ÿ ρ β†’ π’Ÿ (ρ.baseChangeAlong (Ο† : A β†’+* B) hΟ†) of_baseChangeAlong_injective : βˆ€ ⦃A B : Type⦄ [CommRing A] [IsLocalRing A] [Algebra π’ͺ A] [CommRing B] [IsLocalRing B] [Algebra π’ͺ B], IsArtinianTestAlgebra π’ͺ A β†’ IsArtinianTestAlgebra π’ͺ B β†’ βˆ€ (Ο† : A →ₐ[π’ͺ] B) (hΟ† : IsLocalHom (Ο† : A β†’+* B)), Function.Injective Ο† β†’ βˆ€ ⦃ρ : GaloisRepAdic A⦄, π’Ÿ (ρ.baseChangeAlong (Ο† : A β†’+* B) hΟ†) β†’ π’Ÿ ρ of_fibreProduct : βˆ€ ⦃A B C P : Type⦄ [CommRing A] [IsLocalRing A] [Algebra π’ͺ A] [CommRing B] [IsLocalRing B] [Algebra π’ͺ B] [CommRing C] [IsLocalRing C] [Algebra π’ͺ C] [CommRing P] [IsLocalRing P] [Algebra π’ͺ P], IsArtinianTestAlgebra π’ͺ A β†’ IsArtinianTestAlgebra π’ͺ B β†’ IsArtinianTestAlgebra π’ͺ C β†’ IsArtinianTestAlgebra π’ͺ P β†’ βˆ€ (f : A →ₐ[π’ͺ] C) (g : B →ₐ[π’ͺ] C) (pA : P →ₐ[π’ͺ] A) (pB : P →ₐ[π’ͺ] B) (hpA : IsLocalHom (pA : P β†’+* A)) (hpB : IsLocalHom (pB : P β†’+* B)), f.comp pA = g.comp pB β†’ Function.Injective (fun x => (pA x, pB x)) β†’ (βˆ€ a b, f a = g b β†’ βˆƒ x, pA x = a ∧ pB x = b) β†’ βˆ€ ⦃ρ : GaloisRepAdic P⦄, π’Ÿ (ρ.baseChangeAlong (pA : P β†’+* A) hpA) β†’ π’Ÿ (ρ.baseChangeAlong (pB : P β†’+* B) hpB) β†’ π’Ÿ ρ iff_forall_surjective : βˆ€ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [IsNoetherianRing A] [IsAdicComplete (maximalIdeal A) A] [Algebra π’ͺ A], IsLocalHom (algebraMap π’ͺ A) β†’ Function.Surjective (IsLocalRing.residue A ∘ algebraMap π’ͺ A) β†’ βˆ€ (ρ : GaloisRepAdic A), π’Ÿ ρ ↔ βˆ€ ⦃B : Type⦄ [CommRing B] [IsLocalRing B] [Algebra π’ͺ B], IsArtinianTestAlgebra π’ͺ B β†’ βˆ€ (q : A →ₐ[π’ͺ] B) (hq : IsLocalHom (q : A β†’+* B)), Function.Surjective q β†’ π’Ÿ (ρ.baseChangeAlong (q : A β†’+* B) hq) def TangentFinite (ρbar : ResidualGaloisRep (ResidueField π’ͺ)) (π’Ÿ : βˆ€ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [Algebra π’ͺ A], GaloisRepAdic A β†’ Prop) : Prop := letI : Algebra π’ͺ (DualNumber (ResidueField π’ͺ)) := ((algebraMap (ResidueField π’ͺ) (DualNumber (ResidueField π’ͺ))).comp (algebraMap π’ͺ (ResidueField π’ͺ))).toAlgebra letI : Algebra (ResidueField π’ͺ) (ResidueField (DualNumber (ResidueField π’ͺ))) := ((IsLocalRing.residue (DualNumber (ResidueField π’ͺ))).comp (algebraMap (ResidueField π’ͺ) (DualNumber (ResidueField π’ͺ)))).toAlgebra Finite (Quotient (⟨fun ρ ρ' : {ρ : GaloisRepAdic (DualNumber (ResidueField π’ͺ)) // π’Ÿ ρ ∧ ρ.residual.IsEquiv (ρbar.baseChange (ResidueField (DualNumber (ResidueField π’ͺ)))) } => ρ.1.IsEquiv ρ'.1, ⟨fun ρ => ⟨GaloisRepAdic.Equiv.refl ρ.1⟩, fun ⟨e⟩ => ⟨e.symm⟩, fun ⟨e⟩ ⟨e'⟩ => ⟨e.trans e'⟩⟩⟩ : Setoid _)) end GaloisRep end