Theorems · Definition · commutative algebra
AdicCompletion.ofAlgEquiv
{S : Type u_5} → [inst : CommRing S] → (I : Ideal S) → [IsAdicComplete I S] → S ≃ₐ[S] AdicCompletion I SWhen S is I-adic complete, the canonical map from S to
its I-adic completion is an S-algebra isomorphism.
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingIsAdicComplete
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHom.idproof · cited by 18,349
- CommRingstatement and proof · cited by 17,173
- Idealstatement and proof · cited by 4,748
- LinearEquivproof · cited by 3,317
- AlgEquivstatement · cited by 1,681
- LinearEquiv.toLinearMapproof · cited by 1,171
- AddHom.toFunproof · cited by 168
- LinearMap.toAddHomproof · cited by 165
- AdicCompletionstatement and proof · cited by 160
- IsAdicCompletestatement and proof · cited by 124
- LinearEquiv.invFunproof · cited by 29
- AdicCompletion.ofLinearEquivproof · cited by 5
Cited by13
Results whose statement or proof uses this declaration.
- IsAdicComplete.liftRingHomproof · cited by 6
- AdicCompletion.of_ofAlgEquiv_symmstatement · cited by 3
- IsAdicComplete.mk_liftRingHomproof · cited by 2
- AdicCompletion.mk_ofAlgEquiv_symmstatement and proof · cited by 2
- IsAdicComplete.liftAlgHomproof · cited by 2
- AdicCompletion.ofAlgEquiv_applystatement and proof · cited by 2
- AdicCompletion.mk_ofAlgEquiv_symm_eq_evalOneₐstatement and proof · cited by 1
- AdicCompletion.mk_smul_top_ofAlgEquiv_symmstatement and proof · cited by 1
- IsAdicComplete.ofAlgEquiv_comp_liftRingHomstatement · cited by 0
- IsAdicComplete.algHom_extproof · cited by 0
- Algebra.FormallySmooth.exists_mkₐ_comp_eq_of_isAdicCompleteproof · cited by 0
- AdicCompletion.ofAlgEquiv_symm_ofstatement · cited by 0