theorem algebraMap_withVal_continuous_general {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] {B : Type u_4} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) : Continuous (⇑(WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation L 𝔮)).symm ∘ ⇑(algebraMap K L) ∘ ⇑(WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K 𝔭)))

theorem AdicCompletionAlgebra.continuous_algebraMap_adicCompletion {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] {B : Type u_4} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) : Continuous ⇑((algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)).comp ((algebraMap K L).comp (WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K 𝔭)).toRingHom))

noncomputable def AdicCompletionAlgebra.adicCompletionMap {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] {B : Type u_4} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) : IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭 →+* IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮

theorem AdicCompletionAlgebra.adicCompletionMap_comp_algebraMap {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] {B : Type u_4} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) : (adicCompletionMap K 𝔭 𝔮 h𝔮_over_𝔭).comp (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭)) = (algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)).comp (algebraMap K L)

@[reducible]

noncomputable def instAlgebraAdicCompletionOfLiesOver {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] {B : Type u_4} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)

theorem isScalarTower_adicCompletion {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] {B : Type u_4} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) : IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)