InvariantEtaleNeighborhood.lean

theorem flatCoefficient_selectedFactor
    {B : CommRingCat.{u}} {R : Type u} [CommRing R] [Algebra B R]
    {G : Type w} [Group G] [Finite G] [MulSemiringAction G R]
    [SMulCommClass G B R] [Algebra.IsInvariant B R G]
    (C : Under B) [Module.Flat B C]
    {ι : Type u} [Fintype ι] (σ : G →* Equiv.Perm ι)
    (e : ι → (C ⊗[B] R)) (he : CompleteOrthogonalIdempotents e)
    (hinj : Function.Injective (algebraMap B R)) :
    let : MulSemiringAction G (C ⊗[B] R) := baseChangeAction B C R G
    let : SMulCommClass G C (C ⊗[B] R) := baseChangeAction_smulCommClass B C R G
    (∀ (g : G) (i : ι), g • e i = e (σ g i)) →
    ∀ i : ι, (∀ j : ι, ∃ g : G, σ g i = j) →
      let eH : FixedPoints.subalgebra C (C ⊗[B] R) (MulAction.stabilizer G (e i)) :=
        ⟨e i, fun g => g.property⟩
      Function.Bijective (algebraMap C (Localization.Away eH)) ∧
        Algebra.Etale C (Localization.Away eH) := by
  intro actualAction actualComm hσ i htrans eH
  have : Algebra.IsInvariant C (C ⊗[B] R) G := baseChangeAction_isInvariant B C R G
  have hbij : Function.Bijective (algebraMap C (Localization.Away eH)) :=
    algebraMap_away_bijective_of_transitive_completeOrthogonalIdempotents C (C ⊗[B] R) G
      σ e he hσ i htrans (Algebra.TensorProduct.includeLeft_injective (R := B) (S := C) hinj)
  exact ⟨hbij, Algebra.Etale.of_equiv
    (AlgEquiv.ofBijective (Algebra.ofId C (Localization.Away eH)) hbij)⟩

theorem selectedFactor_exists_etale_away
    {B : CommRingCat.{u}} {R : Type u} [CommRing R] [Algebra B R]
    {G : Type w} [Group G] [Finite G] [MulSemiringAction G R] [SMulCommClass G B R]
    (C : Under B) [Algebra.Etale B C] :
    let : MulSemiringAction G (C ⊗[B] R) := baseChangeAction B C R G
    let : SMulCommClass G C (C ⊗[B] R) := baseChangeAction_smulCommClass B C R G
    ∀ (Q : PrimeSpectrum (C ⊗[B] R)) (e : FixedPoints.subalgebra C (C ⊗[B] R) G),
      (e : C ⊗[B] R) ∉ Q.asIdeal → Algebra.Etale C (Localization.Away e) →
      ∃ f : FixedPoints.subalgebra B R G,
        f ∉ (PrimeSpectrum.comap
          ((Algebra.TensorProduct.includeRight (R := B) (A := C) (B := R)).toRingHom.comp
            (FixedPoints.subalgebra B R G).val.toRingHom) Q).asIdeal ∧
          Algebra.Etale B (Localization.Away f) := by
  intro actualAction actualComm Q e he hfactor
  let S := FixedPoints.subalgebra B R G
  let K := Localization.Away e
  let : Algebra S K := (invariantFlatBaseChangeFactorMap B C R G e).toAlgebra
  have : IsScalarTower B S K := IsScalarTower.of_algebraMap_eq (fun b =>
    (IsScalarTower.algebraMap_apply B C K b).trans
      (RingHom.congr_fun (invariantFlatBaseChangeFactorMap_comp_algebraMap B C R G e) b).symm)
  have : Algebra.Etale S K := invariantFlatBaseChangeFactorMap_etale B C R G e
  have : Algebra.Etale C K := hfactor
  have : Algebra.Etale B K := Algebra.Etale.comp B C K
  obtain ⟨P, hP⟩ := invariantFactorNeighborhood_exists_point B C R G Q e he
  exact SchemeTheory.exists_etale_away_of_mem_image_etale_source B S K
    (PrimeSpectrum.comap
      ((Algebra.TensorProduct.includeRight (R := B) (A := C) (B := R)).toRingHom.comp
        (FixedPoints.subalgebra B R G).val.toRingHom) Q) ⟨P, hP⟩

theorem etaleCoefficient_family
    {Ω : Type u} [Field Ω] [IsSepClosed Ω] (φ : B →+* Ω)
    {ι : Type u} [Fintype ι] (σ : G →* Equiv.Perm ι)
    (e : ι → ((geometricStalkSmallAlgebraCocone φ).pt ⊗[B] R))
    (he : CompleteOrthogonalIdempotents e)
    (hσ : ∀ (g : G) (i : ι), g • e i = e (σ g i)) :
    ∃ C : Under B, Algebra.Etale B C ∧
      ∃ (γ : C ⟶ (geometricStalkSmallAlgebraCocone φ).pt) (eC : ι → (C ⊗[B] R)),
        CompleteOrthogonalIdempotents eC ∧
          (∀ (g : G) (i : ι), g • eC i = eC (σ g i)) ∧
          ∀ i, Algebra.TensorProduct.map (CommRingCat.toAlgHom γ) (AlgHom.id B R) (eC i) = e i

theorem algebraic_inertiaNeighborhood
    [Algebra.IsInvariant B R G]
    (A C : Under B) [HenselianLocalRing A] [IsSepClosed (IsLocalRing.ResidueField A)]
    [Module.Flat B A] [Algebra.Etale B C] (γ : C ⟶ A)
    (hfinite : ((IsLocalRing.maximalIdeal A).primesOver (A ⊗[B] R)).Finite)
    [Fintype ((IsLocalRing.maximalIdeal A).primesOver (A ⊗[B] R))]
    (e : ((IsLocalRing.maximalIdeal A).primesOver (A ⊗[B] R)) → (A ⊗[B] R))
    (he : CompleteOrthogonalIdempotents e)
    (hsupp : ∀ (q : (IsLocalRing.maximalIdeal A).primesOver (A ⊗[B] R)) (Q : Ideal (A ⊗[B] R)),
      Q.IsPrime → Q.LiesOver (IsLocalRing.maximalIdeal A) → (e q ∉ Q ↔ Q = q.val))
    (eC : ((IsLocalRing.maximalIdeal A).primesOver (A ⊗[B] R)) → (C ⊗[B] R))
    (heC : CompleteOrthogonalIdempotents eC)
    (hσC : ∀ (g : G) (q : (IsLocalRing.maximalIdeal A).primesOver (A ⊗[B] R)),
      g • eC q = eC (primeFiberPermutation A (A ⊗[B] R) G (IsLocalRing.maximalIdeal A) g q))
    (hmap : ∀ q, Algebra.TensorProduct.map (CommRingCat.toAlgHom γ) (AlgHom.id B R) (eC q) = e q)
    (q : (IsLocalRing.maximalIdeal A).primesOver (A ⊗[B] R))
    (hinj : Function.Injective (algebraMap B R)) :
    ∃ f : FixedPoints.subalgebra B R (q.val.inertia G),
      f ∉ (PrimeSpectrum.comap
        ((Algebra.TensorProduct.includeRight (R := B) (A := A) (B := R)).toRingHom.comp
          (FixedPoints.subalgebra B R (q.val.inertia G)).val.toRingHom)
        ⟨q.val, inferInstance⟩).asIdeal ∧ Algebra.Etale B (Localization.Away f)

theorem invariantGeometricFiber_exists_etale_inertiaNeighborhood
    (R : Type u) (G : Type w) [CommRing R] [Group G] [Finite G] [MulSemiringAction G R]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω] (φ : FixedPoints.subring R G →+* Ω) :
    let B : CommRingCat.{u} := CommRingCat.of (FixedPoints.subring R G)
    let ψ : B →+* Ω := φ
    let A : Under B := (geometricStalkSmallAlgebraCocone ψ).pt
    let : Algebra B A := EtaleFundamentalGroups.underCommRingCatAlgebra A
    let : HenselianLocalRing A :=
      geometricStalk_henselianLocalRing (Spec.map (CommRingCat.ofHom ψ))
    let : IsSepClosed (IsLocalRing.ResidueField A) :=
      geometricStalk_residueField_isSepClosed (Spec.map (CommRingCat.ofHom ψ))
    let T := A ⊗[B] R
    let : MulSemiringAction G T := baseChangeAction B A R G
    let : SMulCommClass G A T := baseChangeAction_smulCommClass B A R G
    ∀ q : (IsLocalRing.maximalIdeal A).primesOver T,
      ∃ f : FixedPoints.subalgebra B R (q.val.inertia G),
        f ∉ (PrimeSpectrum.comap
          ((Algebra.TensorProduct.includeRight (R := B) (A := A) (B := R)).toRingHom.comp
            (FixedPoints.subalgebra B R (q.val.inertia G)).val.toRingHom)
          ⟨q.val, inferInstance⟩).asIdeal ∧ Algebra.Etale B (Localization.Away f) := by
  classical
  intro B ψ A actualAlgebra actualHenselian actualResidue T actualAction actualComm q
  have : Algebra.IsInvariant B R G := by
    constructor
    intro r hr
    exact ⟨⟨r, hr⟩, rfl⟩
  have : Module.Flat B A := geometricStalkStructureMap_flat ψ
  have : Algebra.IsInvariant A T G := baseChangeAction_isInvariant B A R G
  have : Algebra.IsIntegral A T := Algebra.IsInvariant.isIntegral A T G
  have hfinite : ((IsLocalRing.maximalIdeal A).primesOver T).Finite :=
    baseChangeAction_finite_primesOver B A R G (IsLocalRing.maximalIdeal A)
  let : Fintype ((IsLocalRing.maximalIdeal A).primesOver T) := hfinite.fintype
  obtain ⟨e, he, hsupp⟩ := exists_completeOrthogonalIdempotents_of_finite_integral_fiber A T hfinite
  have hσ := isolatingIdempotents_equivariant A T G hfinite e he.idem hsupp
  obtain ⟨C, hC, γ, eC, heC, hσC, hmap⟩ := etaleCoefficient_family ψ
    (primeFiberPermutation A T G (IsLocalRing.maximalIdeal A)) e he hσ
  let : Algebra B C := EtaleFundamentalGroups.underCommRingCatAlgebra C
  have : Algebra.Etale B C := hC
  exact algebraic_inertiaNeighborhood A C γ hfinite e he hsupp eC heC hσC hmap q
    (show Function.Injective (algebraMap B R) from Subtype.val_injective)

theorem inertia_invariants_exists_etale_away
    (R : Type u) (G : Type w) [CommRing R] [Group G] [Finite G] [MulSemiringAction G R]
    (q : Ideal R) [q.IsPrime] :
    ∃ f : FixedPoints.subalgebra (FixedPoints.subring R G) R (q.inertia G),
      (f : R) ∉ q ∧ Algebra.Etale (FixedPoints.subring R G) (Localization.Away f)