Definitions/Def_AlgebraicGeometry_RegularLocalRingFaithfullyFlatDescent.lean

import Mathlib

set_option autoImplicit false

noncomputable section

universe u v

open IsLocalRing

namespace FaithfullyFlatRegularDescent

section StructureDescent

variable (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]

theorem isNoetherianRing_of_faithfullyFlat [Module.FaithfullyFlat A B] [IsNoetherianRing B] :
    IsNoetherianRing A := by
  rw [isNoetherianRing_iff, isNoetherian_iff'] at *
  exact StrictMono.wellFoundedGT (f := fun I : Ideal A => I.map (algebraMap A B))
    (fun I J h => lt_of_le_of_ne (Ideal.map_mono h.le)
      (fun heq => h.ne (by
        have heq' : Ideal.map (algebraMap A B) I = Ideal.map (algebraMap A B) J := heq
        rw [← Ideal.comap_map_eq_self_of_faithfullyFlat (B := B) I,
          ← Ideal.comap_map_eq_self_of_faithfullyFlat (B := B) J, heq'])))

theorem isLocalRing_of_faithfullyFlat [Module.FaithfullyFlat A B] [IsLocalRing B] :
    IsLocalRing A := by
  haveI : Nontrivial A := (algebraMap A B).domain_nontrivial

  have key : ∀ m : Ideal A, m.IsMaximal → m = (maximalIdeal B).comap (algebraMap A B) := by
    intro m hm
    obtain ⟨P, hcomap⟩ := PrimeSpectrum.comap_surjective_of_faithfullyFlat (A := A) (B := B)
      ⟨m, hm.isPrime⟩
    have hPm : P.asIdeal.comap (algebraMap A B) = m := by
      have := congrArg PrimeSpectrum.asIdeal hcomap
      simpa using this
    have hle : m ≤ (maximalIdeal B).comap (algebraMap A B) := by
      rw [← hPm]
      exact Ideal.comap_mono (IsLocalRing.le_maximalIdeal P.isPrime.ne_top)
    refine hm.eq_of_le ?_ hle
    intro htop
    have h1 : (1 : A) ∈ (maximalIdeal B).comap (algebraMap A B) := htop ▸ Submodule.mem_top
    rw [Ideal.mem_comap, map_one] at h1
    exact (maximalIdeal B).ne_top_iff_one.mp (Ideal.IsPrime.ne_top inferInstance) h1
  apply IsLocalRing.of_unique_max_ideal
  obtain ⟨m₀, hm₀⟩ := Ideal.exists_maximal A
  exact ⟨m₀, hm₀, fun J hJ => (key J hJ).trans (key m₀ hm₀).symm⟩

theorem isLocalHom_algebraMap_of_faithfullyFlat [Module.FaithfullyFlat A B]
    [IsLocalRing A] [IsLocalRing B] : IsLocalHom (algebraMap A B) := by
  constructor
  intro a ha
  by_contra h
  have hmem : a ∈ maximalIdeal A := by rwa [mem_maximalIdeal, mem_nonunits_iff]
  obtain ⟨P, hP, hlies⟩ :=
    Ideal.exists_isPrime_liesOver_of_faithfullyFlat (B := B) (maximalIdeal A)
  haveI := hP
  haveI := hlies
  have hin : algebraMap A B a ∈ P := by
    have hover := P.over_def (maximalIdeal A)
    rw [hover] at hmem
    exact hmem
  exact hP.ne_top (P.eq_top_of_isUnit_mem hin ha)

theorem ringKrullDim_le_of_faithfullyFlat [Module.FaithfullyFlat A B] :
    ringKrullDim A ≤ ringKrullDim B := by
  rw [ringKrullDim, ringKrullDim, Order.krullDim, iSup_le_iff]
  intro l
  obtain ⟨P, hP, hlies⟩ :=
    Ideal.exists_isPrime_liesOver_of_faithfullyFlat (B := B) l.last.asIdeal
  haveI := hP
  haveI := hlies
  obtain ⟨L, hlen, -, -⟩ := Ideal.exists_ltSeries_of_hasGoingDown l P
  calc (l.length : WithBot ℕ∞) = (L.length : WithBot ℕ∞) := by rw [hlen]
    _ ≤ Order.krullDim (PrimeSpectrum B) := Order.LTSeries.length_le_krullDim L

end StructureDescent

section ValuationTargetEngine

variable (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]

theorem exists_span_image_eq_span_singleton [IsDomain B] [ValuationRing B]
    (s : Finset A) (hs : s.Nonempty) :
    ∃ x ∈ s, Ideal.span ((algebraMap A B) '' s) = Ideal.span {algebraMap A B x} := by
  classical
  induction s using Finset.induction_on with
  | empty => exact absurd hs (by simp)
  | insert a t ha ih =>
    by_cases ht : t.Nonempty
    · obtain ⟨x, hxt, hx⟩ := ih ht
      have htot := (ValuationRing.iff_ideal_total.mp ‹_›).total
        (Ideal.span {algebraMap A B a}) (Ideal.span {algebraMap A B x})
      have himg : (algebraMap A B) '' (insert a t : Finset A) =
          insert (algebraMap A B a) ((algebraMap A B) '' t) := by
        simp [Finset.coe_insert, Set.image_insert_eq]
      rcases htot with hle | hle
      · refine ⟨x, by simp [hxt], ?_⟩
        rw [himg, Ideal.span_insert, hx, sup_eq_right.mpr hle]
      · refine ⟨a, by simp, ?_⟩
        rw [himg, Ideal.span_insert, hx, sup_eq_left.mpr hle]
    · rw [Finset.not_nonempty_iff_eq_empty] at ht
      subst ht
      exact ⟨a, by simp, by simp [Set.image_singleton]⟩

theorem maximalIdeal_isPrincipal_of_faithfullyFlat [Module.FaithfullyFlat A B]
    [IsNoetherianRing A] [IsLocalRing A] [IsDomain B] [ValuationRing B] :
    (maximalIdeal A).IsPrincipal := by
  classical
  obtain ⟨s, hs⟩ := IsNoetherian.noetherian (maximalIdeal A)
  by_cases hs0 : s = ∅
  · refine ⟨⟨0, ?_⟩⟩
    rw [← hs, hs0]
    simp
  · obtain ⟨x, hxs, hx⟩ :=
      exists_span_image_eq_span_singleton A B s (Finset.nonempty_of_ne_empty hs0)
    refine ⟨⟨x, ?_⟩⟩
    have h1 : (maximalIdeal A).map (algebraMap A B) = (Ideal.span {x}).map (algebraMap A B) := by
      rw [← hs, Ideal.submodule_span_eq, Ideal.map_span, Ideal.map_span, Set.image_singleton, hx]
    have h2 := Ideal.comap_map_eq_self_of_faithfullyFlat (B := B) (maximalIdeal A)
    have h3 := Ideal.comap_map_eq_self_of_faithfullyFlat (B := B) (Ideal.span {x})
    rw [← h2, h1, h3, Ideal.submodule_span_eq]

theorem isRegularLocalRing_of_faithfullyFlat_of_valuationRing [Module.FaithfullyFlat A B]
    [IsNoetherianRing A] [IsLocalRing A] [IsDomain B] [ValuationRing B] :
    IsRegularLocalRing A := by
  haveI : IsDomain A := IsDomain.of_faithfulSMul A B
  have hp : (maximalIdeal A).IsPrincipal := maximalIdeal_isPrincipal_of_faithfullyFlat A B
  haveI : IsPrincipalIdealRing A :=
    ((tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain A).out 4 0).mp hp
  infer_instance

theorem isRegularLocalRing_of_faithfullyFlat_of_valuationRing' [Module.FaithfullyFlat A B]
    [IsDomain B] [ValuationRing B] [IsNoetherianRing B] :
    IsRegularLocalRing A := by
  haveI : IsLocalRing B := ValuationRing.isLocalRing B
  haveI : IsLocalRing A := isLocalRing_of_faithfullyFlat A B
  haveI : IsNoetherianRing A := isNoetherianRing_of_faithfullyFlat A B
  exact isRegularLocalRing_of_faithfullyFlat_of_valuationRing A B

end ValuationTargetEngine

section Corollaries

variable (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]

theorem isRegularLocalRing_of_faithfullyFlat_of_field (K : Type v) [Field K] [Algebra A K]
    [Module.FaithfullyFlat A K] : IsRegularLocalRing A :=
  isRegularLocalRing_of_faithfullyFlat_of_valuationRing' A K

theorem isRegularLocalRing_of_faithfullyFlat_of_isDiscreteValuationRing
    [Module.FaithfullyFlat A B] [IsDomain B] [IsDiscreteValuationRing B] :
    IsRegularLocalRing A := by
  haveI : ValuationRing B := by
    have h : IsPrincipalIdealRing B := inferInstance
    exact ((tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain B).out 0 1).mp h
  exact isRegularLocalRing_of_faithfullyFlat_of_valuationRing' A B

theorem isField_of_isRegularLocalRing_of_ringKrullDim_eq_zero (R : Type v) [CommRing R]
    [IsRegularLocalRing R] (hdim : ringKrullDim R = 0) : IsField R := by
  rw [IsLocalRing.isField_iff_maximalIdeal_eq]
  have hspan := IsRegularLocalRing.spanFinrank_maximalIdeal (R := R)
  rw [hdim] at hspan
  have h0 : (maximalIdeal R).spanFinrank = 0 := by exact_mod_cast hspan
  exact (Submodule.spanFinrank_eq_zero_iff_eq_bot (IsNoetherian.noetherian _)).mp h0

theorem isRegularLocalRing_of_faithfullyFlat_of_ringKrullDim_eq_zero
    [Module.FaithfullyFlat A B] [IsRegularLocalRing B] (hdim : ringKrullDim B = 0) :
    IsRegularLocalRing A := by
  letI : Field B := (isField_of_isRegularLocalRing_of_ringKrullDim_eq_zero B hdim).toField
  exact isRegularLocalRing_of_faithfullyFlat_of_valuationRing' A B

theorem valuationRing_of_isRegularLocalRing_of_ringKrullDim_le_one (R : Type v) [CommRing R]
    [IsRegularLocalRing R] [IsDomain R] (hdim : ringKrullDim R ≤ 1) : ValuationRing R := by
  have hspan := IsRegularLocalRing.spanFinrank_maximalIdeal (R := R)
  have hle : ((maximalIdeal R).spanFinrank : WithBot ℕ∞) ≤ 1 := hspan.le.trans hdim
  have hle' : (maximalIdeal R).spanFinrank ≤ 1 := by exact_mod_cast hle
  have hcot : Module.finrank (ResidueField R) (CotangentSpace R) ≤ 1 := by
    rw [← spanFinrank_maximalIdeal_eq_finrank_cotangentSpace]
    exact hle'
  exact ((tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain R).out 5 1).mp hcot

theorem isRegularLocalRing_of_faithfullyFlat_of_ringKrullDim_le_one
    [Module.FaithfullyFlat A B] [IsRegularLocalRing B] [IsDomain B]
    (hdim : ringKrullDim B ≤ 1) : IsRegularLocalRing A := by
  haveI : ValuationRing B := valuationRing_of_isRegularLocalRing_of_ringKrullDim_le_one B hdim
  exact isRegularLocalRing_of_faithfullyFlat_of_valuationRing' A B

end Corollaries

section Carrier

def RegularDescendsAlongFaithfullyFlat : Prop :=
  ∀ (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]
    [Module.FaithfullyFlat A B] [IsRegularLocalRing B], IsRegularLocalRing A

def RegularDescendsAlongFlatLocalHom : Prop :=
  ∀ (A : Type u) (B : Type v) [CommRing A] [CommRing B] [IsLocalRing A] [IsNoetherianRing A]
    [Algebra A B] [Module.Flat A B] [IsRegularLocalRing B],
    IsLocalHom (algebraMap A B) → IsRegularLocalRing A

theorem regularDescendsAlongFaithfullyFlat_iff_flatLocalHom :
    RegularDescendsAlongFaithfullyFlat.{u, v} ↔ RegularDescendsAlongFlatLocalHom.{u, v} := by
  constructor
  · intro h A B _ _ _ _ _ _ _ hloc
    haveI := hloc
    haveI : Module.FaithfullyFlat A B := Module.FaithfullyFlat.of_flat_of_isLocalHom
    exact h A B
  · intro h A B _ _ _ _ _
    haveI : IsLocalRing A := isLocalRing_of_faithfullyFlat A B
    haveI : IsNoetherianRing A := isNoetherianRing_of_faithfullyFlat A B
    exact h A B (isLocalHom_algebraMap_of_faithfullyFlat A B)

theorem carrier_holds_for_valuationRing_targets :
    ∀ (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]
      [Module.FaithfullyFlat A B] [IsDomain B] [ValuationRing B] [IsNoetherianRing B],
      IsRegularLocalRing A :=
  fun A B _ _ _ _ _ _ _ => isRegularLocalRing_of_faithfullyFlat_of_valuationRing' A B

end Carrier

section KMWiring

variable (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]

theorem isRegularLocalRing_of_free_of_carrier
    (hcarrier : RegularDescendsAlongFaithfullyFlat.{u, v})
    [Module.Free A B] [Nontrivial B] [IsRegularLocalRing B] :
    IsRegularLocalRing A := by
  haveI : Module.FaithfullyFlat A B := inferInstance
  exact hcarrier A B

theorem isRegularLocalRing_of_free_of_valuationRing
    [Module.Free A B] [Nontrivial B] [IsDomain B] [ValuationRing B] [IsNoetherianRing B] :
    IsRegularLocalRing A := by
  haveI : Module.FaithfullyFlat A B := inferInstance
  exact isRegularLocalRing_of_faithfullyFlat_of_valuationRing' A B

end KMWiring

section SatGates

theorem gate_carrier_hypotheses_rat :
    Module.FaithfullyFlat ℚ ℚ ∧ IsRegularLocalRing ℚ :=
  ⟨inferInstance, inferInstance⟩

theorem gate_carrier_hypotheses_padicInt (p : ℕ) [Fact p.Prime] :
    Module.FaithfullyFlat ℤ_[p] ℤ_[p] ∧ IsRegularLocalRing ℤ_[p] :=
  ⟨inferInstance, inferInstance⟩

theorem gate_descent_engine_rat : IsRegularLocalRing ℚ :=
  isRegularLocalRing_of_faithfullyFlat_of_field ℚ ℚ

theorem gate_descent_engine_padicInt (p : ℕ) [Fact p.Prime] : IsRegularLocalRing ℤ_[p] :=
  isRegularLocalRing_of_faithfullyFlat_of_isDiscreteValuationRing ℤ_[p] ℤ_[p]

theorem gate_carrier_applies_rat (h : RegularDescendsAlongFaithfullyFlat.{0, 0}) :
    IsRegularLocalRing ℚ :=
  h ℚ ℚ

theorem gate_km_wiring_padicInt (p : ℕ) [Fact p.Prime] : IsRegularLocalRing ℤ_[p] :=
  isRegularLocalRing_of_free_of_valuationRing ℤ_[p] ℤ_[p]

end SatGates

section Teeth

open DualNumber

theorem not_isRegularLocalRing_dualNumber : ¬ IsRegularLocalRing (DualNumber ℚ) := by
  intro h

  have heps_ne : (eps : DualNumber ℚ) ≠ 0 := by
    intro heq
    have h1 := congrArg TrivSqZeroExt.snd heq
    simp at h1

  have hnil : nilradical (DualNumber ℚ) = Ideal.span {(eps : DualNumber ℚ)} := by
    rcases DualNumber.ideal_trichotomy (nilradical (DualNumber ℚ)) with h0 | h1 | h2
    · exfalso
      have hin : (eps : DualNumber ℚ) ∈ nilradical (DualNumber ℚ) :=
        mem_nilradical.mpr DualNumber.isNilpotent_eps
      rw [h0] at hin
      exact heps_ne (by simpa using hin)
    · exact h1
    · exfalso
      have hone : IsNilpotent (1 : DualNumber ℚ) :=
        mem_nilradical.mp (h2 ▸ Submodule.mem_top)
      obtain ⟨n, hn⟩ := hone
      rw [one_pow] at hn
      exact one_ne_zero hn
  haveI : (nilradical (DualNumber ℚ)).IsMaximal := by
    rw [hnil]
    exact DualNumber.isMaximal_span_singleton_eps
  haveI : Ring.KrullDimLE 0 (DualNumber ℚ) :=
    Ring.KrullDimLE.of_isMaximal_nilradical (DualNumber ℚ)
  have hdim : ringKrullDim (DualNumber ℚ) = 0 :=
    ringKrullDimZero_iff_ringKrullDim_eq_zero.mp inferInstance

  have hspan := h.spanFinrank_maximalIdeal
  rw [hdim] at hspan
  have hspan0 : (maximalIdeal (DualNumber ℚ)).spanFinrank = 0 := by exact_mod_cast hspan
  have hbot : maximalIdeal (DualNumber ℚ) = ⊥ :=
    (Submodule.spanFinrank_eq_zero_iff_eq_bot (IsNoetherian.noetherian _)).mp hspan0
  rw [DualNumber.maximalIdeal_eq_span_singleton_eps, Ideal.span_singleton_eq_bot] at hbot
  exact heps_ne hbot

set_option synthInstance.maxHeartbeats 400000 in

theorem not_regularDescends_along_surjective_localHom :
    ¬ (∀ (A B : Type) [CommRing A] [CommRing B] [IsLocalRing A] [IsNoetherianRing A]
        [Algebra A B] [IsRegularLocalRing B],
        Function.Surjective (algebraMap A B) → IsLocalHom (algebraMap A B) →
        IsRegularLocalRing A) := by
  intro hclaim
  letI : Algebra (DualNumber ℚ) ℚ := TrivSqZeroExt.algebraBase ℚ ℚ
  haveI : IsNoetherianRing (DualNumber ℚ) := PrincipalIdealRing.isNoetherianRing
  haveI : IsRegularLocalRing ℚ := gate_descent_engine_rat
  refine not_isRegularLocalRing_dualNumber (hclaim (DualNumber ℚ) ℚ ?_ ?_)
  ·
    exact fun r => ⟨TrivSqZeroExt.inl r, TrivSqZeroExt.fst_inl ℚ r⟩
  ·

    exact ⟨fun a ha => TrivSqZeroExt.isUnit_iff_isUnit_fst.mpr ha⟩

set_option synthInstance.maxHeartbeats 400000 in

theorem not_regularAscends_alongFaithfullyFlat :
    ¬ (∀ (A B : Type) [CommRing A] [CommRing B] [Algebra A B] [Module.FaithfullyFlat A B]
        [IsLocalRing B] [IsNoetherianRing B],
        IsRegularLocalRing A → IsRegularLocalRing B) := by
  intro hclaim
  haveI : Module.Free ℚ (DualNumber ℚ) := Module.Free.of_divisionRing ℚ (DualNumber ℚ)
  haveI : IsNoetherianRing (DualNumber ℚ) := PrincipalIdealRing.isNoetherianRing
  exact not_isRegularLocalRing_dualNumber
    (hclaim ℚ (DualNumber ℚ) gate_descent_engine_rat)

end Teeth

end FaithfullyFlatRegularDescent

/--
info: 'FaithfullyFlatRegularDescent.isNoetherianRing_of_faithfullyFlat' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.isNoetherianRing_of_faithfullyFlat

/--
info: 'FaithfullyFlatRegularDescent.isLocalRing_of_faithfullyFlat' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.isLocalRing_of_faithfullyFlat

/--
info: 'FaithfullyFlatRegularDescent.isLocalHom_algebraMap_of_faithfullyFlat' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.isLocalHom_algebraMap_of_faithfullyFlat

/--
info: 'FaithfullyFlatRegularDescent.ringKrullDim_le_of_faithfullyFlat' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.ringKrullDim_le_of_faithfullyFlat

/--
info: 'FaithfullyFlatRegularDescent.maximalIdeal_isPrincipal_of_faithfullyFlat' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.maximalIdeal_isPrincipal_of_faithfullyFlat

/--
info: 'FaithfullyFlatRegularDescent.isRegularLocalRing_of_faithfullyFlat_of_valuationRing' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.isRegularLocalRing_of_faithfullyFlat_of_valuationRing

/--
info: 'FaithfullyFlatRegularDescent.isRegularLocalRing_of_faithfullyFlat_of_valuationRing'' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.isRegularLocalRing_of_faithfullyFlat_of_valuationRing'

/--
info: 'FaithfullyFlatRegularDescent.isRegularLocalRing_of_faithfullyFlat_of_field' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.isRegularLocalRing_of_faithfullyFlat_of_field

/--
info: 'FaithfullyFlatRegularDescent.isRegularLocalRing_of_faithfullyFlat_of_isDiscreteValuationRing' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.isRegularLocalRing_of_faithfullyFlat_of_isDiscreteValuationRing

/--
info: 'FaithfullyFlatRegularDescent.isRegularLocalRing_of_faithfullyFlat_of_ringKrullDim_eq_zero' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.isRegularLocalRing_of_faithfullyFlat_of_ringKrullDim_eq_zero

/--
info: 'FaithfullyFlatRegularDescent.isRegularLocalRing_of_faithfullyFlat_of_ringKrullDim_le_one' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.isRegularLocalRing_of_faithfullyFlat_of_ringKrullDim_le_one

/--
info: 'FaithfullyFlatRegularDescent.regularDescendsAlongFaithfullyFlat_iff_flatLocalHom' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.regularDescendsAlongFaithfullyFlat_iff_flatLocalHom

/--
info: 'FaithfullyFlatRegularDescent.carrier_holds_for_valuationRing_targets' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.carrier_holds_for_valuationRing_targets

/--
info: 'FaithfullyFlatRegularDescent.isRegularLocalRing_of_free_of_carrier' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.isRegularLocalRing_of_free_of_carrier

/--
info: 'FaithfullyFlatRegularDescent.isRegularLocalRing_of_free_of_valuationRing' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.isRegularLocalRing_of_free_of_valuationRing

/--
info: 'FaithfullyFlatRegularDescent.gate_descent_engine_rat' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.gate_descent_engine_rat

/--
info: 'FaithfullyFlatRegularDescent.gate_descent_engine_padicInt' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.gate_descent_engine_padicInt

/--
info: 'FaithfullyFlatRegularDescent.gate_km_wiring_padicInt' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.gate_km_wiring_padicInt

/--
info: 'FaithfullyFlatRegularDescent.not_isRegularLocalRing_dualNumber' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.not_isRegularLocalRing_dualNumber

/--
info: 'FaithfullyFlatRegularDescent.not_regularDescends_along_surjective_localHom' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.not_regularDescends_along_surjective_localHom

/--
info: 'FaithfullyFlatRegularDescent.not_regularAscends_alongFaithfullyFlat' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms FaithfullyFlatRegularDescent.not_regularAscends_alongFaithfullyFlat

end